:: The Reflection Theorem :: by Grzegorz Bancerek :: :: Received August 10, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CLASSES2, ZF_LANG, FUNCT_1, SUBSET_1, ZF_MODEL, TARSKI, ORDINAL1, XBOOLE_0, ZFMISC_1, CARD_1, BVFUNC_2, XBOOLEAN, ZFMODEL1, RELAT_1, ORDINAL2, ORDINAL4, CARD_3, CLASSES1, NUMBERS, NAT_1, ARYTM_3, XXREAL_0, REALSET1, FUNCT_2, ZF_REFLE, CARD_FIL, CARD_5; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, ZF_MODEL, ZFMODEL1, ORDINAL2, NUMBERS, CARD_3, CLASSES1, CLASSES2, ZF_LANG, ORDINAL4, ZF_LANG1, CARD_5, CARD_FIL, CARD_LAR, XXREAL_0; constructors ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, CLASSES1, CARD_3, ORDINAL4, ZF_MODEL, ZFMODEL1, ZF_LANG1, RELSET_1, CARD_LAR, CARD_FIL, CARD_5, NUMBERS; registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, CARD_5, CARD_LAR, CARD_3, RELAT_1; requirements NUMERALS, BOOLE, SUBSET; begin reserve W for Universe, H for ZF-formula, x,y,z,X for set, k for Variable, f for Function of VAR,W, u,v for Element of W; theorem :: ZF_REFLE:1 W |= the_axiom_of_pairs; theorem :: ZF_REFLE:2 W |= the_axiom_of_unions; theorem :: ZF_REFLE:3 omega in W implies W |= the_axiom_of_infinity; theorem :: ZF_REFLE:4 W |= the_axiom_of_power_sets; theorem :: ZF_REFLE:5 for H st { x.0,x.1,x.2 } misses Free H holds W |= the_axiom_of_substitution_for H; theorem :: ZF_REFLE:6 omega in W implies W is being_a_model_of_ZF; reserve F for Function, A,B,C for Ordinal, a,b,b1,b2,c for Ordinal of W, fi for Ordinal-Sequence, phi for Ordinal-Sequence of W, H for ZF-formula; scheme :: ZF_REFLE:sch 1 ALFA9Universe { W()->Universe, D() -> non empty set, P[set,set] }: ex F st dom F = D() & for d being Element of D() ex a being Ordinal of W() st a = F.d & P[d,a] & for b being Ordinal of W() st P[d,b] holds a c= b provided for d being Element of D() ex a being Ordinal of W() st P[d,a]; theorem :: ZF_REFLE:7 x is Ordinal of W iff x in On W; reserve psi for Ordinal-Sequence; scheme :: ZF_REFLE:sch 2 OrdSeqOfUnivEx { W()->Universe, P[object,object] }: ex phi being Ordinal-Sequence of W() st for a being Ordinal of W() holds P[a,phi.a] provided for a being Ordinal of W() ex b being Ordinal of W() st P[a,b]; scheme :: ZF_REFLE:sch 3 UOSExist { W()->Universe, a()->Ordinal of W(), C(Ordinal,Ordinal)->Ordinal of W(), D(Ordinal,Sequence)->Ordinal of W() } : ex phi being Ordinal-Sequence of W() st phi.0-element_of W() = a() & (for a being Ordinal of W() holds phi.( succ a) = C(a,phi.a)) & for a being Ordinal of W() st a <> 0-element_of W() & a is limit_ordinal holds phi.a = D(a,phi|a); scheme :: ZF_REFLE:sch 4 UniverseInd { W()->Universe, P[Ordinal] }: for a being Ordinal of W() holds P[a] provided P[0-element_of W()] and for a being Ordinal of W() st P[a] holds P[succ a] and for a being Ordinal of W() st a <> 0-element_of W() & a is limit_ordinal & for b being Ordinal of W() st b in a holds P[b] holds P[a]; definition let f be Function, W be Universe, a be Ordinal of W; func union(f,a) -> set equals :: ZF_REFLE:def 1 Union (W|`(f|Rank a)); end; theorem :: ZF_REFLE:8 for L being Sequence,A holds L|Rank A is Sequence; theorem :: ZF_REFLE:9 for L being Ordinal-Sequence,A holds L|Rank A is Ordinal-Sequence; theorem :: ZF_REFLE:10 Union psi is Ordinal; theorem :: ZF_REFLE:11 Union (X|`psi) is epsilon-transitive epsilon-connected set; theorem :: ZF_REFLE:12 On Rank A = A; theorem :: ZF_REFLE:13 psi|Rank A = psi|A; definition let phi be Ordinal-Sequence, W be Universe, a be Ordinal of W; redefine func union(phi,a) -> Ordinal of W; end; theorem :: ZF_REFLE:14 for phi being Ordinal-Sequence of W holds union(phi,a) = Union ( phi|a) & union(phi|a,a) = Union (phi|a); definition let W be Universe, a,b be Ordinal of W; redefine func a \/ b -> Ordinal of W; end; registration let W; cluster non empty for Element of W; end; definition let W; mode Subclass of W is non empty Subset of W; end; definition let W; let IT be Sequence of W; attr IT is DOMAIN-yielding means :: ZF_REFLE:def 2 dom IT = On W; end; registration let W; cluster DOMAIN-yielding non-empty for Sequence of W; end; definition let W; mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding Sequence of W; end; definition let W; let L be DOMAIN-Sequence of W; redefine func Union L -> Subclass of W; let a; redefine func L.a -> non empty Element of W; end; reserve L for DOMAIN-Sequence of W, n for Element of NAT, f for Function of VAR,L.a; theorem :: ZF_REFLE:15 a in dom L; theorem :: ZF_REFLE:16 L.a c= Union L; theorem :: ZF_REFLE:17 NAT,VAR are_equipotent; theorem :: ZF_REFLE:18 sup X c= succ union On X; theorem :: ZF_REFLE:19 X in W implies sup X in W; reserve x1 for Variable; ::\$N Reflection Theorem theorem :: ZF_REFLE:20 omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a)) implies for H ex phi st phi is increasing & phi is continuous & for a st phi.a = a & {} <> a for f holds Union L,(Union L)!f |= H iff L.a,f |= H; begin :: Addenda :: from CARD_LAR, 2010.03.11, A.T. reserve M for non countable Aleph; theorem :: ZF_REFLE:21 M is strongly_inaccessible implies Rank M is being_a_model_of_ZF;