:: ZF_REFLE semantic presentation begin theorem Th1: :: ZF_REFLE:1 for W being Universe holds W |= the_axiom_of_pairs proof let W be Universe; ::_thesis: W |= the_axiom_of_pairs for u, v being Element of W holds {u,v} in W ; hence W |= the_axiom_of_pairs by ZFMODEL1:2; ::_thesis: verum end; theorem Th2: :: ZF_REFLE:2 for W being Universe holds W |= the_axiom_of_unions proof let W be Universe; ::_thesis: W |= the_axiom_of_unions for u being Element of W holds union u in W ; hence W |= the_axiom_of_unions by ZFMODEL1:4; ::_thesis: verum end; theorem Th3: :: ZF_REFLE:3 for W being Universe st omega in W holds W |= the_axiom_of_infinity proof let W be Universe; ::_thesis: ( omega in W implies W |= the_axiom_of_infinity ) assume omega in W ; ::_thesis: W |= the_axiom_of_infinity then reconsider u = omega as Element of W ; now__::_thesis:_ex_u_being_Element_of_W_st_ (_u_<>_{}_&_(_for_v_being_Element_of_W_st_v_in_u_holds_ ex_w_being_Element_of_W_st_ (_v_c<_w_&_w_in_u_)_)_) take u = u; ::_thesis: ( u <> {} & ( for v being Element of W st v in u holds ex w being Element of W st ( v c< w & w in u ) ) ) thus u <> {} ; ::_thesis: for v being Element of W st v in u holds ex w being Element of W st ( v c< w & w in u ) let v be Element of W; ::_thesis: ( v in u implies ex w being Element of W st ( v c< w & w in u ) ) assume A1: v in u ; ::_thesis: ex w being Element of W st ( v c< w & w in u ) then reconsider A = v as Ordinal ; succ A in omega by A1, ORDINAL1:28; then succ A c= u by ORDINAL1:def_2; then reconsider w = succ A as Element of W by CLASSES1:def_1; take w = w; ::_thesis: ( v c< w & w in u ) A in succ A by ORDINAL1:6; then ( v c= w & v <> w ) by ORDINAL1:def_2; hence ( v c< w & w in u ) by A1, ORDINAL1:28, XBOOLE_0:def_8; ::_thesis: verum end; hence W |= the_axiom_of_infinity by ZFMODEL1:6; ::_thesis: verum end; theorem Th4: :: ZF_REFLE:4 for W being Universe holds W |= the_axiom_of_power_sets proof let W be Universe; ::_thesis: W |= the_axiom_of_power_sets now__::_thesis:_for_u_being_Element_of_W_holds_W_/\_(bool_u)_in_W let u be Element of W; ::_thesis: W /\ (bool u) in W W /\ (bool u) c= bool u by XBOOLE_1:17; hence W /\ (bool u) in W by CLASSES1:def_1; ::_thesis: verum end; hence W |= the_axiom_of_power_sets by ZFMODEL1:8; ::_thesis: verum end; theorem Th5: :: ZF_REFLE:5 for W being Universe for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds W |= the_axiom_of_substitution_for H proof let W be Universe; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds W |= the_axiom_of_substitution_for H for H being ZF-formula for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of W holds (def_func' (H,f)) .: u in W proof let H be ZF-formula; ::_thesis: for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of W holds (def_func' (H,f)) .: u in W let f be Function of VAR,W; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of W holds (def_func' (H,f)) .: u in W ) assume that {(x. 0),(x. 1),(x. 2)} misses Free H and W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for u being Element of W holds (def_func' (H,f)) .: u in W let u be Element of W; ::_thesis: (def_func' (H,f)) .: u in W card u in card W by CLASSES2:1; then card ((def_func' (H,f)) .: u) in card W by CARD_1:67, ORDINAL1:12; hence (def_func' (H,f)) .: u in W by CLASSES1:1; ::_thesis: verum end; hence for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds W |= the_axiom_of_substitution_for H by ZFMODEL1:15; ::_thesis: verum end; theorem Th6: :: ZF_REFLE:6 for W being Universe st omega in W holds W is being_a_model_of_ZF proof let W be Universe; ::_thesis: ( omega in W implies W is being_a_model_of_ZF ) assume omega in W ; ::_thesis: W is being_a_model_of_ZF hence ( W is epsilon-transitive & W |= the_axiom_of_pairs & W |= the_axiom_of_unions & W |= the_axiom_of_infinity & W |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds W |= the_axiom_of_substitution_for H ) ) by Th1, Th2, Th3, Th4, Th5; :: according to ZF_MODEL:def_12 ::_thesis: verum end; scheme :: ZF_REFLE:sch 1 ALFA9Universe{ F1() -> Universe, F2() -> non empty set , P1[ set , set ] } : ex F being Function st ( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) ) ) provided A1: for d being Element of F2() ex a being Ordinal of F1() st P1[d,a] proof A2: for d being Element of F2() ex A being Ordinal st P1[d,A] proof let d be Element of F2(); ::_thesis: ex A being Ordinal st P1[d,A] consider a being Ordinal of F1() such that A3: P1[d,a] by A1; reconsider a = a as Ordinal ; take a ; ::_thesis: P1[d,a] thus P1[d,a] by A3; ::_thesis: verum end; consider F being Function such that A4: dom F = F2() and A5: for d being Element of F2() ex A being Ordinal st ( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds A c= B ) ) from ORDINAL1:sch_6(A2); take F ; ::_thesis: ( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) ) ) thus dom F = F2() by A4; ::_thesis: for d being Element of F2() ex a being Ordinal of F1() st ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) let d be Element of F2(); ::_thesis: ex a being Ordinal of F1() st ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) consider A being Ordinal such that A6: ( A = F . d & P1[d,A] ) and A7: for B being Ordinal st P1[d,B] holds A c= B by A5; consider a being Ordinal of F1() such that A8: P1[d,a] by A1; A c= a by A7, A8; then reconsider a = A as Ordinal of F1() by CLASSES1:def_1; take a ; ::_thesis: ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) thus ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds a c= b ) ) by A6, A7; ::_thesis: verum end; theorem :: ZF_REFLE:7 for W being Universe for x being set holds ( x is Ordinal of W iff x in On W ) by ORDINAL1:def_9; scheme :: ZF_REFLE:sch 2 OrdSeqOfUnivEx{ F1() -> Universe, P1[ set , set ] } : ex phi being Ordinal-Sequence of F1() st for a being Ordinal of F1() holds P1[a,phi . a] provided A1: for a being Ordinal of F1() ex b being Ordinal of F1() st P1[a,b] proof defpred S1[ set , set ] means ( P1[$1,$2] & $2 is Ordinal of F1() ); A2: for x being set st x in On F1() holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in On F1() implies ex y being set st S1[x,y] ) assume x in On F1() ; ::_thesis: ex y being set st S1[x,y] then reconsider a = x as Ordinal of F1() by ORDINAL1:def_9; consider b being Ordinal of F1() such that A3: P1[a,b] by A1; reconsider y = b as set ; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A3; ::_thesis: verum end; consider f being Function such that A4: ( dom f = On F1() & ( for x being set st x in On F1() holds S1[x,f . x] ) ) from CLASSES1:sch_1(A2); reconsider phi = f as T-Sequence by A4, ORDINAL1:def_7; A5: rng phi c= On F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in On F1() ) assume x in rng phi ; ::_thesis: x in On F1() then ex y being set st ( y in dom phi & x = phi . y ) by FUNCT_1:def_3; then reconsider x = x as Ordinal of F1() by A4; x in F1() ; hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum end; then reconsider phi = phi as Ordinal-Sequence by ORDINAL2:def_4; reconsider phi = phi as Ordinal-Sequence of F1() by A4, A5, FUNCT_2:def_1, RELSET_1:4; take phi ; ::_thesis: for a being Ordinal of F1() holds P1[a,phi . a] let a be Ordinal of F1(); ::_thesis: P1[a,phi . a] a in On F1() by ORDINAL1:def_9; hence P1[a,phi . a] by A4; ::_thesis: verum end; scheme :: ZF_REFLE:sch 3 UOSExist{ F1() -> Universe, F2() -> Ordinal of F1(), F3( Ordinal, Ordinal) -> Ordinal of F1(), F4( Ordinal, T-Sequence) -> Ordinal of F1() } : ex phi being Ordinal-Sequence of F1() st ( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds phi . a = F4(a,(phi | a)) ) ) proof consider phi being Ordinal-Sequence such that A1: dom phi = On F1() and A2: ( {} in On F1() implies phi . {} = F2() ) and A3: for A being Ordinal st succ A in On F1() holds phi . (succ A) = F3(A,(phi . A)) and A4: for A being Ordinal st A in On F1() & A <> {} & A is limit_ordinal holds phi . A = F4(A,(phi | A)) from ORDINAL2:sch_11(); rng phi c= On F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in On F1() ) assume x in rng phi ; ::_thesis: x in On F1() then consider y being set such that A5: y in dom phi and A6: x = phi . y by FUNCT_1:def_3; reconsider y = y as Ordinal of F1() by A1, A5, ORDINAL1:def_9; A7: now__::_thesis:_(_(_for_A_being_Ordinal_holds_not_y_=_succ_A_)_&_y_<>_{}_implies_x_in_On_F1()_) assume for A being Ordinal holds not y = succ A ; ::_thesis: ( y <> {} implies x in On F1() ) then A8: y is limit_ordinal by ORDINAL1:29; assume y <> {} ; ::_thesis: x in On F1() then x = F4(y,(phi | y)) by A1, A4, A5, A6, A8; hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum end; now__::_thesis:_(_ex_A_being_Ordinal_st_y_=_succ_A_implies_x_in_On_F1()_) given A being Ordinal such that A9: y = succ A ; ::_thesis: x in On F1() reconsider B = phi . A as Ordinal ; x = F3(A,B) by A1, A3, A5, A6, A9; hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum end; hence x in On F1() by A2, A6, A7, ORDINAL1:def_9; ::_thesis: verum end; then reconsider phi = phi as Ordinal-Sequence of F1() by A1, FUNCT_2:def_1, RELSET_1:4; take phi ; ::_thesis: ( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds phi . a = F4(a,(phi | a)) ) ) 0-element_of F1() in dom phi by ORDINAL4:34; hence phi . (0-element_of F1()) = F2() by A1, A2, ORDINAL4:33; ::_thesis: ( ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds phi . a = F4(a,(phi | a)) ) ) thus for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) by A1, A3, ORDINAL4:34; ::_thesis: for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds phi . a = F4(a,(phi | a)) let a be Ordinal of F1(); ::_thesis: ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) ) ( a in dom phi & {} = 0-element_of F1() ) by ORDINAL4:33, ORDINAL4:34; hence ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) ) by A4; ::_thesis: verum end; scheme :: ZF_REFLE:sch 4 UniverseInd{ F1() -> Universe, P1[ Ordinal] } : for a being Ordinal of F1() holds P1[a] provided A1: P1[ 0-element_of F1()] and A2: for a being Ordinal of F1() st P1[a] holds P1[ succ a] and A3: for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal & ( for b being Ordinal of F1() st b in a holds P1[b] ) holds P1[a] proof defpred S1[ Ordinal] means ( $1 is Ordinal of F1() implies P1[$1] ); A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds S1[B] ) holds S1[A] proof let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds S1[B] ) implies S1[A] ) assume that A5: ( A <> {} & A is limit_ordinal ) and A6: for B being Ordinal st B in A & B is Ordinal of F1() holds P1[B] ; ::_thesis: S1[A] assume A is Ordinal of F1() ; ::_thesis: P1[A] then reconsider a = A as Ordinal of F1() ; ( {} = 0-element_of F1() & ( for b being Ordinal of F1() st b in a holds P1[b] ) ) by A6, ORDINAL4:33; hence P1[A] by A3, A5; ::_thesis: verum end; A7: for A being Ordinal st S1[A] holds S1[ succ A] proof let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] ) assume that A8: ( A is Ordinal of F1() implies P1[A] ) and A9: succ A is Ordinal of F1() ; ::_thesis: P1[ succ A] ( A in succ A & succ A in On F1() ) by A9, ORDINAL1:6, ORDINAL1:def_9; then A in On F1() by ORDINAL1:10; then reconsider a = A as Ordinal of F1() by ORDINAL1:def_9; P1[ succ a] by A2, A8; hence P1[ succ A] ; ::_thesis: verum end; A10: S1[ {} ] by A1, ORDINAL4:33; for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A7, A4); hence for a being Ordinal of F1() holds P1[a] ; ::_thesis: verum end; definition let f be Function; let W be Universe; let a be Ordinal of W; func union (f,a) -> set equals :: ZF_REFLE:def 1 Union (W |` (f | (Rank a))); correctness coherence Union (W |` (f | (Rank a))) is set ; ; end; :: deftheorem defines union ZF_REFLE:def_1_:_ for f being Function for W being Universe for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a))); theorem Th8: :: ZF_REFLE:8 for L being T-Sequence for A being Ordinal holds L | (Rank A) is T-Sequence proof let L be T-Sequence; ::_thesis: for A being Ordinal holds L | (Rank A) is T-Sequence let A be Ordinal; ::_thesis: L | (Rank A) is T-Sequence A1: dom (L | (Rank A)) = (dom L) /\ (Rank A) by RELAT_1:61; now__::_thesis:_for_X_being_set_st_X_in_dom_(L_|_(Rank_A))_holds_ (_X_is_Ordinal_&_X_c=_dom_(L_|_(Rank_A))_) let X be set ; ::_thesis: ( X in dom (L | (Rank A)) implies ( X is Ordinal & X c= dom (L | (Rank A)) ) ) assume A2: X in dom (L | (Rank A)) ; ::_thesis: ( X is Ordinal & X c= dom (L | (Rank A)) ) then A3: X in dom L by A1, XBOOLE_0:def_4; hence X is Ordinal ; ::_thesis: X c= dom (L | (Rank A)) X in Rank A by A1, A2, XBOOLE_0:def_4; then A4: X c= Rank A by ORDINAL1:def_2; X c= dom L by A3, ORDINAL1:def_2; hence X c= dom (L | (Rank A)) by A1, A4, XBOOLE_1:19; ::_thesis: verum end; then dom (L | (Rank A)) is Ordinal by ORDINAL1:19; hence L | (Rank A) is T-Sequence by ORDINAL1:31; ::_thesis: verum end; theorem Th9: :: ZF_REFLE:9 for L being Ordinal-Sequence for A being Ordinal holds L | (Rank A) is Ordinal-Sequence proof let L be Ordinal-Sequence; ::_thesis: for A being Ordinal holds L | (Rank A) is Ordinal-Sequence let A be Ordinal; ::_thesis: L | (Rank A) is Ordinal-Sequence reconsider K = L | (Rank A) as T-Sequence by Th8; consider B being Ordinal such that A1: rng L c= B by ORDINAL2:def_4; rng K c= rng L by RELAT_1:70; then rng K c= B by A1, XBOOLE_1:1; hence L | (Rank A) is Ordinal-Sequence by ORDINAL2:def_4; ::_thesis: verum end; theorem :: ZF_REFLE:10 for psi being Ordinal-Sequence holds Union psi is Ordinal ; theorem Th11: :: ZF_REFLE:11 for X being set for psi being Ordinal-Sequence holds Union (X |` psi) is Ordinal proof let X be set ; ::_thesis: for psi being Ordinal-Sequence holds Union (X |` psi) is Ordinal let psi be Ordinal-Sequence; ::_thesis: Union (X |` psi) is Ordinal consider A being Ordinal such that A1: rng psi c= A by ORDINAL2:def_4; A2: rng (X |` psi) c= rng psi by RELAT_1:87; A3: now__::_thesis:_for_x_being_set_st_x_in_rng_(X_|`_psi)_holds_ x_is_Ordinal let x be set ; ::_thesis: ( x in rng (X |` psi) implies x is Ordinal ) assume x in rng (X |` psi) ; ::_thesis: x is Ordinal then x in A by A1, A2, TARSKI:def_3; hence x is Ordinal ; ::_thesis: verum end; Union (X |` psi) = union (rng (X |` psi)) by CARD_3:def_4; hence Union (X |` psi) is Ordinal by A3, ORDINAL1:23; ::_thesis: verum end; theorem Th12: :: ZF_REFLE:12 for A being Ordinal holds On (Rank A) = A proof let A be Ordinal; ::_thesis: On (Rank A) = A thus On (Rank A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= On (Rank A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On (Rank A) or x in A ) assume A1: x in On (Rank A) ; ::_thesis: x in A then reconsider B = x as Ordinal by ORDINAL1:def_9; x in Rank A by A1, ORDINAL1:def_9; then the_rank_of B in A by CLASSES1:66; hence x in A by CLASSES1:73; ::_thesis: verum end; On A c= On (Rank A) by CLASSES1:38, ORDINAL2:9; hence A c= On (Rank A) by ORDINAL2:8; ::_thesis: verum end; theorem Th13: :: ZF_REFLE:13 for A being Ordinal for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A proof let A be Ordinal; ::_thesis: for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A let psi be Ordinal-Sequence; ::_thesis: psi | (Rank A) = psi | A dom (psi | (Rank A)) c= dom psi by RELAT_1:60; then ( On (dom (psi | (Rank A))) c= On (Rank A) & On (dom (psi | (Rank A))) = dom (psi | (Rank A)) ) by ORDINAL2:9, ORDINAL3:6, RELAT_1:58; then A1: dom (psi | (Rank A)) c= A by Th12; A c= Rank A by CLASSES1:38; then (psi | (Rank A)) | A = psi | A by FUNCT_1:51; hence psi | (Rank A) = psi | A by A1, RELAT_1:68; ::_thesis: verum end; definition let phi be Ordinal-Sequence; let W be Universe; let a be Ordinal of W; :: original: union redefine func union (phi,a) -> Ordinal of W; coherence union (phi,a) is Ordinal of W proof reconsider K = phi | (Rank a) as Ordinal-Sequence by Th9; reconsider A = Union (W |` K) as Ordinal by Th11; a in On W by ORDINAL1:def_9; then ( dom K c= Rank a & Rank a in W ) by CLASSES2:25, RELAT_1:58; then ( dom (W |` K) c= dom K & dom K in W ) by CLASSES1:def_1, FUNCT_1:56; then dom (W |` K) in W by CLASSES1:def_1; then A1: card (dom (W |` K)) in card W by CLASSES2:1; (W |` K) .: (dom (W |` K)) = rng (W |` K) by RELAT_1:113; then ( rng (W |` K) c= W & card (rng (W |` K)) in card W ) by A1, CARD_1:67, ORDINAL1:12, RELAT_1:85; then A2: rng (W |` K) in W by CLASSES1:1; union (rng (W |` K)) = Union (W |` K) by CARD_3:def_4; then A in W by A2, CLASSES2:59; hence union (phi,a) is Ordinal of W ; ::_thesis: verum end; end; theorem Th14: :: ZF_REFLE:14 for W being Universe for a being Ordinal of W for phi being Ordinal-Sequence of W holds ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) proof let W be Universe; ::_thesis: for a being Ordinal of W for phi being Ordinal-Sequence of W holds ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) let a be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W holds ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) let phi be Ordinal-Sequence of W; ::_thesis: ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) On W c= W by ORDINAL2:7; then ( rng (phi | a) c= rng phi & rng phi c= W ) by XBOOLE_1:1, RELAT_1:70; then ( a c= Rank a & phi | a = W |` (phi | a) ) by CLASSES1:38, RELAT_1:94, XBOOLE_1:1; hence ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) by Th13, FUNCT_1:51; ::_thesis: verum end; definition let W be Universe; let a, b be Ordinal of W; :: original: \/ redefine funca \/ b -> Ordinal of W; coherence a \/ b is Ordinal of W proof ( a c= b or b c= a ) ; hence a \/ b is Ordinal of W by XBOOLE_1:12; ::_thesis: verum end; end; registration let W be Universe; cluster non empty for Element of W; existence not for b1 being Element of W holds b1 is empty proof set u = the Element of W; { the Element of W} is non empty Element of W ; hence not for b1 being Element of W holds b1 is empty ; ::_thesis: verum end; end; definition let W be Universe; mode Subclass of W is non empty Subset of W; end; definition let W be Universe; let IT be T-Sequence of W; attrIT is DOMAIN-yielding means :Def2: :: ZF_REFLE:def 2 dom IT = On W; end; :: deftheorem Def2 defines DOMAIN-yielding ZF_REFLE:def_2_:_ for W being Universe for IT being T-Sequence of W holds ( IT is DOMAIN-yielding iff dom IT = On W ); registration let W be Universe; cluster Relation-like non-empty W -valued T-Sequence-like Function-like DOMAIN-yielding for set ; existence ex b1 being T-Sequence of W st ( b1 is DOMAIN-yielding & b1 is non-empty ) proof set D = the non empty Element of W; deffunc H1( set ) -> non empty Element of W = the non empty Element of W; consider L being T-Sequence such that A1: ( dom L = On W & ( for A being Ordinal for L1 being T-Sequence st A in On W & L1 = L | A holds L . A = H1(L1) ) ) from ORDINAL1:sch_4(); rng L c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in W ) assume x in rng L ; ::_thesis: x in W then consider y being set such that A2: y in dom L and A3: x = L . y by FUNCT_1:def_3; reconsider y = y as Ordinal by A2; L | y = L | y ; then x = the non empty Element of W by A1, A2, A3; hence x in W ; ::_thesis: verum end; then reconsider L = L as T-Sequence of W by RELAT_1:def_19; take L ; ::_thesis: ( L is DOMAIN-yielding & L is non-empty ) thus dom L = On W by A1; :: according to ZF_REFLE:def_2 ::_thesis: L is non-empty assume {} in rng L ; :: according to RELAT_1:def_9 ::_thesis: contradiction then consider x being set such that A4: x in dom L and A5: {} = L . x by FUNCT_1:def_3; reconsider x = x as Ordinal by A4; L | x = L | x ; hence contradiction by A1, A4, A5; ::_thesis: verum end; end; definition let W be Universe; mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W; end; definition let W be Universe; let L be DOMAIN-Sequence of W; :: original: Union redefine func Union L -> Subclass of W; coherence Union L is Subclass of W proof set a = the Ordinal of W; the Ordinal of W in On W by ORDINAL1:def_9; then the Ordinal of W in dom L by Def2; then L . the Ordinal of W in rng L by FUNCT_1:def_3; then ( L . the Ordinal of W c= union (rng L) & L . the Ordinal of W <> {} ) by RELAT_1:def_9, ZFMISC_1:74; then union (rng L) <> {} ; then reconsider S = Union L as non empty set by CARD_3:def_4; ( rng L c= W & Union L = union (rng L) ) by CARD_3:def_4; then A1: Union L c= union W by ZFMISC_1:77; S c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in W ) assume x in S ; ::_thesis: x in W then consider X being set such that A2: x in X and A3: X in W by A1, TARSKI:def_4; X c= W by A3, ORDINAL1:def_2; hence x in W by A2; ::_thesis: verum end; hence Union L is Subclass of W ; ::_thesis: verum end; let a be Ordinal of W; :: original: . redefine funcL . a -> non empty Element of W; coherence L . a is non empty Element of W proof a in On W by ORDINAL1:def_9; then a in dom L by Def2; then A4: L . a in rng L by FUNCT_1:def_3; thus L . a is non empty Element of W by A4, RELAT_1:def_9; ::_thesis: verum end; end; theorem Th15: :: ZF_REFLE:15 for W being Universe for a being Ordinal of W for L being DOMAIN-Sequence of W holds a in dom L proof let W be Universe; ::_thesis: for a being Ordinal of W for L being DOMAIN-Sequence of W holds a in dom L let a be Ordinal of W; ::_thesis: for L being DOMAIN-Sequence of W holds a in dom L let L be DOMAIN-Sequence of W; ::_thesis: a in dom L a in On W by ORDINAL1:def_9; hence a in dom L by Def2; ::_thesis: verum end; theorem Th16: :: ZF_REFLE:16 for W being Universe for a being Ordinal of W for L being DOMAIN-Sequence of W holds L . a c= Union L proof let W be Universe; ::_thesis: for a being Ordinal of W for L being DOMAIN-Sequence of W holds L . a c= Union L let a be Ordinal of W; ::_thesis: for L being DOMAIN-Sequence of W holds L . a c= Union L let L be DOMAIN-Sequence of W; ::_thesis: L . a c= Union L a in dom L by Th15; then A1: L . a in rng L by FUNCT_1:def_3; union (rng L) = Union L by CARD_3:def_4; hence L . a c= Union L by A1, ZFMISC_1:74; ::_thesis: verum end; theorem Th17: :: ZF_REFLE:17 NAT , VAR are_equipotent proof deffunc H1( Nat, set ) -> Element of NAT = 5 + ($1 + 1); consider f being Function of NAT,NAT such that A1: ( f . 0 = 5 + 0 & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12(); A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_=_5_+_n let n be Element of NAT ; ::_thesis: f . n = 5 + n ( ex j being Nat st n = j + 1 implies f . n = 5 + n ) by A1; then ( n = 0 or f . n = 5 + n ) by NAT_1:6; hence f . n = 5 + n by A1; ::_thesis: verum end; A3: dom f = NAT by FUNCT_2:def_1; thus NAT , VAR are_equipotent ::_thesis: verum proof reconsider g = f as Function ; take g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & dom g = NAT & rng g = VAR ) thus g is one-to-one ::_thesis: ( dom g = NAT & rng g = VAR ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y ) assume ( x in dom g & y in dom g ) ; ::_thesis: ( not g . x = g . y or x = y ) then reconsider n1 = x, n2 = y as Element of NAT by FUNCT_2:def_1; ( f . n1 = 5 + n1 & f . n2 = 5 + n2 ) by A2; hence ( not g . x = g . y or x = y ) by XCMPLX_1:2; ::_thesis: verum end; thus dom g = NAT by FUNCT_2:def_1; ::_thesis: rng g = VAR thus rng g c= VAR :: according to XBOOLE_0:def_10 ::_thesis: VAR c= rng g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in VAR ) assume x in rng g ; ::_thesis: x in VAR then consider y being set such that A4: y in dom f and A5: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A4; A6: 5 + y >= 5 by NAT_1:11; x = 5 + y by A2, A5; hence x in VAR by A6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VAR or x in rng g ) assume x in VAR ; ::_thesis: x in rng g then ex n being Element of NAT st ( x = n & 5 <= n ) ; then consider n being Nat such that A7: x = 5 + n by NAT_1:10; A8: n in NAT by ORDINAL1:def_12; then f . n = x by A2, A7; hence x in rng g by A3, A8, FUNCT_1:def_3; ::_thesis: verum end; end; theorem :: ZF_REFLE:18 for X being set holds sup X c= succ (union (On X)) by ORDINAL3:72; theorem Th19: :: ZF_REFLE:19 for W being Universe for X being set st X in W holds sup X in W proof let W be Universe; ::_thesis: for X being set st X in W holds sup X in W let X be set ; ::_thesis: ( X in W implies sup X in W ) reconsider a = union (On X) as Ordinal by ORDINAL3:5; A1: On X c= X by ORDINAL2:7; assume X in W ; ::_thesis: sup X in W then On X in W by A1, CLASSES1:def_1; then reconsider a = a as Ordinal of W by CLASSES2:59; sup X c= succ a by ORDINAL3:72; hence sup X in W by CLASSES1:def_1; ::_thesis: verum end; theorem :: ZF_REFLE:20 for W being Universe for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds for H being ZF-formula ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) proof let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) holds for H being ZF-formula ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ) implies for H being ZF-formula ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) ) assume that A1: omega in W and A2: for a, b being Ordinal of W st a in b holds L . a c= L . b and A3: for a being Ordinal of W st a <> {} & a is limit_ordinal holds L . a = Union (L | a) ; ::_thesis: for H being ZF-formula ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) set M = Union L; A4: union (rng L) = Union L by CARD_3:def_4; defpred S1[ ZF-formula] means ex phi being Ordinal-Sequence of W st ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= $1 iff L . a,f |= $1 ) ) ); A5: dom L = On W by Def2; A6: for H being ZF-formula st H is universal & S1[ the_scope_of H] holds S1[H] proof deffunc H1( Ordinal of W, Ordinal-Sequence) -> Ordinal of W = union ($2,$1); let H be ZF-formula; ::_thesis: ( H is universal & S1[ the_scope_of H] implies S1[H] ) set x0 = bound_in H; set H9 = the_scope_of H; defpred S2[ set , set ] means ex f being Function of VAR,(Union L) st ( $1 = f & ( ex m being Element of Union L st ( m in L . $2 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( $2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ); assume H is universal ; ::_thesis: ( not S1[ the_scope_of H] or S1[H] ) then A7: H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44; A8: for h being Element of Funcs (VAR,(Union L)) ex a being Ordinal of W st S2[h,a] proof let h be Element of Funcs (VAR,(Union L)); ::_thesis: ex a being Ordinal of W st S2[h,a] reconsider f = h as Element of Funcs (VAR,(Union L)) ; reconsider f = f as Function of VAR,(Union L) ; now__::_thesis:_ex_a_being_Ordinal_of_W_st_S2[h,a] percases ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) or ex m being Element of Union L st Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ; suppose for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: ex a being Ordinal of W st S2[h,a] hence ex a being Ordinal of W st S2[h,a] ; ::_thesis: verum end; supposeA9: ex m being Element of Union L st Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: ex a being Ordinal of W st S2[h,a] thus ex a being Ordinal of W st S2[h,a] ::_thesis: verum proof consider m being Element of Union L such that A10: Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) by A9; consider X being set such that A11: m in X and A12: X in rng L by A4, TARSKI:def_4; consider x being set such that A13: x in dom L and A14: X = L . x by A12, FUNCT_1:def_3; reconsider x = x as Ordinal by A13; reconsider b = x as Ordinal of W by A5, A13, ORDINAL1:def_9; take b ; ::_thesis: S2[h,b] take f ; ::_thesis: ( h = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) thus ( h = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) by A10, A11, A14; ::_thesis: verum end; end; end; end; hence ex a being Ordinal of W st S2[h,a] ; ::_thesis: verum end; consider rho being Function such that A15: dom rho = Funcs (VAR,(Union L)) and A16: for h being Element of Funcs (VAR,(Union L)) ex a being Ordinal of W st ( a = rho . h & S2[h,a] & ( for b being Ordinal of W st S2[h,b] holds a c= b ) ) from ZF_REFLE:sch_1(A8); defpred S3[ Ordinal of W, Ordinal of W] means $2 = sup (rho .: (Funcs (VAR,(L . $1)))); A17: for a being Ordinal of W ex b being Ordinal of W st S3[a,b] proof let a be Ordinal of W; ::_thesis: ex b being Ordinal of W st S3[a,b] set X = rho .: (Funcs (VAR,(L . a))); A18: rho .: (Funcs (VAR,(L . a))) c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rho .: (Funcs (VAR,(L . a))) or x in W ) assume x in rho .: (Funcs (VAR,(L . a))) ; ::_thesis: x in W then consider h being set such that h in dom rho and A19: h in Funcs (VAR,(L . a)) and A20: x = rho . h by FUNCT_1:def_6; Funcs (VAR,(L . a)) c= Funcs (VAR,(Union L)) by Th16, FUNCT_5:56; then reconsider h = h as Element of Funcs (VAR,(Union L)) by A19; ex a being Ordinal of W st ( a = rho . h & ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . a & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds a c= b ) ) by A16; hence x in W by A20; ::_thesis: verum end; Funcs (omega,(L . a)) in W by A1, CLASSES2:61; then A21: card (Funcs (omega,(L . a))) in card W by CLASSES2:1; ( card VAR = card omega & card (L . a) = card (L . a) ) by Th17, CARD_1:5; then card (Funcs (VAR,(L . a))) = card (Funcs (omega,(L . a))) by FUNCT_5:61; then card (rho .: (Funcs (VAR,(L . a)))) in card W by A21, CARD_1:67, ORDINAL1:12; then rho .: (Funcs (VAR,(L . a))) in W by A18, CLASSES1:1; then reconsider b = sup (rho .: (Funcs (VAR,(L . a)))) as Ordinal of W by Th19; take b ; ::_thesis: S3[a,b] thus S3[a,b] ; ::_thesis: verum end; consider si being Ordinal-Sequence of W such that A22: for a being Ordinal of W holds S3[a,si . a] from ZF_REFLE:sch_2(A17); deffunc H2( Ordinal of W, Ordinal of W) -> Element of W = succ ((si . (succ $1)) \/ $2); consider ksi being Ordinal-Sequence of W such that A23: ksi . (0-element_of W) = si . (0-element_of W) and A24: for a being Ordinal of W holds ksi . (succ a) = H2(a,ksi . a) and A25: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds ksi . a = H1(a,ksi | a) from ZF_REFLE:sch_3(); defpred S4[ Ordinal] means si . $1 c= ksi . $1; given phi being Ordinal-Sequence of W such that A26: phi is increasing and A27: phi is continuous and A28: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= the_scope_of H iff L . a,f |= the_scope_of H ) ; ::_thesis: S1[H] A29: ksi is increasing proof let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds ( not A in b1 or not b1 in dom ksi or ksi . A in ksi . b1 ) let B be Ordinal; ::_thesis: ( not A in B or not B in dom ksi or ksi . A in ksi . B ) assume that A30: A in B and A31: B in dom ksi ; ::_thesis: ksi . A in ksi . B A in dom ksi by A30, A31, ORDINAL1:10; then reconsider a = A, b = B as Ordinal of W by A31, ORDINAL1:def_9; defpred S5[ Ordinal of W] means ( a in $1 implies ksi . a in ksi . $1 ); A32: for c being Ordinal of W st S5[c] holds S5[ succ c] proof let c be Ordinal of W; ::_thesis: ( S5[c] implies S5[ succ c] ) assume that A33: ( a in c implies ksi . a in ksi . c ) and A34: a in succ c ; ::_thesis: ksi . a in ksi . (succ c) A35: a c= c by A34, ORDINAL1:22; A36: ( ksi . a in ksi . c or ksi . a = ksi . c ) proof percases ( a <> c or a = c ) ; suppose a <> c ; ::_thesis: ( ksi . a in ksi . c or ksi . a = ksi . c ) then a c< c by A35, XBOOLE_0:def_8; hence ( ksi . a in ksi . c or ksi . a = ksi . c ) by A33, ORDINAL1:11; ::_thesis: verum end; suppose a = c ; ::_thesis: ( ksi . a in ksi . c or ksi . a = ksi . c ) hence ( ksi . a in ksi . c or ksi . a = ksi . c ) ; ::_thesis: verum end; end; end; A37: ksi . c c= (si . (succ c)) \/ (ksi . c) by XBOOLE_1:7; ( ksi . (succ c) = succ ((si . (succ c)) \/ (ksi . c)) & (si . (succ c)) \/ (ksi . c) in succ ((si . (succ c)) \/ (ksi . c)) ) by A24, ORDINAL1:22; hence ksi . a in ksi . (succ c) by A37, A36, ORDINAL1:10, ORDINAL1:12; ::_thesis: verum end; A38: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds S5[c] ) holds S5[b] proof ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) by A24; then (si . (succ a)) \/ (ksi . a) in ksi . (succ a) by ORDINAL1:6; then A39: ksi . a in ksi . (succ a) by ORDINAL1:12, XBOOLE_1:7; let b be Ordinal of W; ::_thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds S5[c] ) implies S5[b] ) assume that A40: b <> 0-element_of W and A41: b is limit_ordinal and for c being Ordinal of W st c in b holds S5[c] and A42: a in b ; ::_thesis: ksi . a in ksi . b ( succ a in dom ksi & succ a in b ) by A41, A42, ORDINAL1:28, ORDINAL4:34; then A43: ksi . (succ a) in rng (ksi | b) by FUNCT_1:50; ksi . b = union ((ksi | b),b) by A25, A40, A41 .= Union (ksi | b) by Th14 .= union (rng (ksi | b)) by CARD_3:def_4 ; hence ksi . a in ksi . b by A43, A39, TARSKI:def_4; ::_thesis: verum end; A44: S5[ 0-element_of W] by ORDINAL4:33; for c being Ordinal of W holds S5[c] from ZF_REFLE:sch_4(A44, A32, A38); then ksi . a in ksi . b by A30; hence ksi . A in ksi . B ; ::_thesis: verum end; A45: 0-element_of W = {} by ORDINAL4:33; A46: ksi is continuous proof let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds ( not A in dom ksi or A = {} or not A is limit_ordinal or not b1 = ksi . A or b1 is_limes_of ksi | A ) let B be Ordinal; ::_thesis: ( not A in dom ksi or A = {} or not A is limit_ordinal or not B = ksi . A or B is_limes_of ksi | A ) assume that A47: A in dom ksi and A48: A <> {} and A49: A is limit_ordinal and A50: B = ksi . A ; ::_thesis: B is_limes_of ksi | A A c= dom ksi by A47, ORDINAL1:def_2; then A51: dom (ksi | A) = A by RELAT_1:62; reconsider a = A as Ordinal of W by A47, ORDINAL1:def_9; A52: B = union ((ksi | a),a) by A25, A45, A48, A49, A50 .= Union (ksi | a) by Th14 .= union (rng (ksi | a)) by CARD_3:def_4 ; A53: B c= sup (ksi | A) proof let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in B or C in sup (ksi | A) ) assume C in B ; ::_thesis: C in sup (ksi | A) then consider X being set such that A54: C in X and A55: X in rng (ksi | A) by A52, TARSKI:def_4; rng (ksi | A) c= rng ksi by RELAT_1:70; then X in rng ksi by A55; then reconsider X = X as Ordinal ; X in sup (ksi | A) by A55, ORDINAL2:19; hence C in sup (ksi | A) by A54, ORDINAL1:10; ::_thesis: verum end; A56: ksi | A is increasing by A29, ORDINAL4:15; A57: sup (ksi | A) c= B proof let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in sup (ksi | A) or C in B ) assume C in sup (ksi | A) ; ::_thesis: C in B then consider D being Ordinal such that A58: D in rng (ksi | A) and A59: C c= D by ORDINAL2:21; consider x being set such that A60: x in dom (ksi | A) and A61: D = (ksi | A) . x by A58, FUNCT_1:def_3; reconsider x = x as Ordinal by A60; A62: succ x in A by A49, A60, ORDINAL1:28; then A63: (ksi | A) . (succ x) in rng (ksi | A) by A51, FUNCT_1:def_3; x in succ x by ORDINAL1:6; then D in (ksi | A) . (succ x) by A51, A56, A61, A62, ORDINAL2:def_12; then D in B by A52, A63, TARSKI:def_4; hence C in B by A59, ORDINAL1:12; ::_thesis: verum end; sup (ksi | A) is_limes_of ksi | A by A48, A49, A51, A56, ORDINAL4:8; hence B is_limes_of ksi | A by A53, A57, XBOOLE_0:def_10; ::_thesis: verum end; A64: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds si . a c= sup (si | a) proof let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal implies si . a c= sup (si | a) ) defpred S5[ set ] means $1 in Free ('not' (the_scope_of H)); assume that A65: a <> 0-element_of W and A66: a is limit_ordinal ; ::_thesis: si . a c= sup (si | a) A67: si . a = sup (rho .: (Funcs (VAR,(L . a)))) by A22; let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in si . a or A in sup (si | a) ) assume A in si . a ; ::_thesis: A in sup (si | a) then consider B being Ordinal such that A68: B in rho .: (Funcs (VAR,(L . a))) and A69: A c= B by A67, ORDINAL2:21; consider x being set such that A70: x in dom rho and A71: x in Funcs (VAR,(L . a)) and A72: B = rho . x by A68, FUNCT_1:def_6; reconsider h = x as Element of Funcs (VAR,(Union L)) by A15, A70; consider a1 being Ordinal of W such that A73: a1 = rho . h and A74: ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and A75: for b being Ordinal of W st ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds a1 c= b by A16; consider f being Function of VAR,(Union L) such that A76: h = f and A77: ( ex m being Element of Union L st ( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) by A74; defpred S6[ set , set ] means for a being Ordinal of W st f . $1 in L . a holds f . $2 in L . a; A78: now__::_thesis:_(_Free_('not'_(the_scope_of_H))_<>_{}_implies_ex_x_being_Ordinal_of_W_st_ (_x_in_a_&_(_for_y_being_Variable_st_y_in_Free_('not'_(the_scope_of_H))_holds_ f_._y_in_L_._x_)_)_) A79: for x, y being set holds ( S6[x,y] or S6[y,x] ) proof let x, y be set ; ::_thesis: ( S6[x,y] or S6[y,x] ) given a being Ordinal of W such that A80: ( f . x in L . a & not f . y in L . a ) ; ::_thesis: S6[y,x] let b be Ordinal of W; ::_thesis: ( f . y in L . b implies f . x in L . b ) assume A81: f . y in L . b ; ::_thesis: f . x in L . b ( a in b or a = b or b in a ) by ORDINAL1:14; then ( L . a c= L . b or L . b c= L . a ) by A2; hence f . x in L . b by A80, A81; ::_thesis: verum end; assume Free ('not' (the_scope_of H)) <> {} ; ::_thesis: ex x being Ordinal of W st ( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds f . y in L . x ) ) then A82: Free ('not' (the_scope_of H)) <> {} ; A83: ( L . a = Union (L | a) & Union (L | a) = union (rng (L | a)) ) by A3, A45, A65, A66, CARD_3:def_4; A84: for x, y, z being set st S6[x,y] & S6[y,z] holds S6[x,z] ; consider z being set such that A85: ( z in Free ('not' (the_scope_of H)) & ( for y being set st y in Free ('not' (the_scope_of H)) holds S6[z,y] ) ) from CARD_2:sch_2(A82, A79, A84); reconsider z = z as Variable by A85; A86: dom (L | a) c= a by RELAT_1:58; A87: ex s being Function st ( f = s & dom s = VAR & rng s c= L . a ) by A71, A76, FUNCT_2:def_2; then f . z in rng f by FUNCT_1:def_3; then consider X being set such that A88: f . z in X and A89: X in rng (L | a) by A87, A83, TARSKI:def_4; consider x being set such that A90: x in dom (L | a) and A91: X = (L | a) . x by A89, FUNCT_1:def_3; A92: (L | a) . x = L . x by A90, FUNCT_1:47; reconsider x = x as Ordinal by A90; a in On W by ORDINAL1:def_9; then x in On W by A90, A86, ORDINAL1:10; then reconsider x = x as Ordinal of W by ORDINAL1:def_9; take x = x; ::_thesis: ( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds f . y in L . x ) ) thus x in a by A90, A86; ::_thesis: for y being Variable st y in Free ('not' (the_scope_of H)) holds f . y in L . x let y be Variable; ::_thesis: ( y in Free ('not' (the_scope_of H)) implies f . y in L . x ) assume y in Free ('not' (the_scope_of H)) ; ::_thesis: f . y in L . x hence f . y in L . x by A85, A88, A91, A92; ::_thesis: verum end; now__::_thesis:_(_Free_('not'_(the_scope_of_H))_=_{}_implies_ex_b_being_Element_of_W_st_ (_b_in_a_&_(_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_ f_._x1_in_L_._b_)_)_) assume A93: Free ('not' (the_scope_of H)) = {} ; ::_thesis: ex b being Element of W st ( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds f . x1 in L . b ) ) take b = 0-element_of W; ::_thesis: ( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds f . x1 in L . b ) ) thus b in a by A45, A65, ORDINAL3:8; ::_thesis: for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds f . x1 in L . b thus for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds f . x1 in L . b by A93; ::_thesis: verum end; then consider c being Ordinal of W such that A94: c in a and A95: for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds f . x1 in L . c by A78; A96: si . c = sup (rho .: (Funcs (VAR,(L . c)))) by A22; ( c in dom si & dom (si | a) = (dom si) /\ a ) by ORDINAL4:34, RELAT_1:61; then A97: c in dom (si | a) by A94, XBOOLE_0:def_4; si . c = (si | a) . c by A94, FUNCT_1:49; then si . c in rng (si | a) by A97, FUNCT_1:def_3; then A98: si . c in sup (si | a) by ORDINAL2:19; deffunc H3( set ) -> set = f . $1; set e = the Element of L . c; deffunc H4( set ) -> Element of L . c = the Element of L . c; consider v being Function such that A99: ( dom v = VAR & ( for x being set st x in VAR holds ( ( S5[x] implies v . x = H3(x) ) & ( not S5[x] implies v . x = H4(x) ) ) ) ) from PARTFUN1:sch_1(); A100: rng v c= L . c proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng v or x in L . c ) assume x in rng v ; ::_thesis: x in L . c then consider y being set such that A101: y in dom v and A102: x = v . y by FUNCT_1:def_3; reconsider y = y as Variable by A99, A101; ( y in Free ('not' (the_scope_of H)) or not y in Free ('not' (the_scope_of H)) ) ; then ( ( x = f . y & f . y in L . c ) or x = the Element of L . c ) by A95, A99, A102; hence x in L . c ; ::_thesis: verum end; then reconsider v = v as Function of VAR,(L . c) by A99, FUNCT_2:def_1, RELSET_1:4; A103: v in Funcs (VAR,(L . c)) by A99, A100, FUNCT_2:def_2; Funcs (VAR,(L . c)) c= Funcs (VAR,(Union L)) by Th16, FUNCT_5:56; then reconsider v9 = v as Element of Funcs (VAR,(Union L)) by A103; consider a2 being Ordinal of W such that A104: a2 = rho . v9 and A105: ex f being Function of VAR,(Union L) st ( v9 = f & ( ex m being Element of Union L st ( m in L . a2 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and A106: for b being Ordinal of W st ex f being Function of VAR,(Union L) st ( v9 = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds a2 c= b by A16; consider f9 being Function of VAR,(Union L) such that A107: v9 = f9 and A108: ( ex m being Element of Union L st ( m in L . a2 & Union L,f9 / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f9 / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) by A105; A109: v = (Union L) ! v by Th16, ZF_LANG1:def_1; A110: now__::_thesis:_(_ex_m_being_Element_of_Union_L_st_ (_m_in_L_._a1_&_Union_L,f_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H)_)_implies_a1_=_a2_) given m being Element of Union L such that A111: m in L . a1 and A112: Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: a1 = a2 A113: now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_ (f_/_((bound_in_H),m))_._x1_=_(((Union_L)_!_v)_/_((bound_in_H),m))_._x1 let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 ) A114: (f / ((bound_in H),m)) . (bound_in H) = m by FUNCT_7:128; A115: ( x1 <> bound_in H implies ( (f / ((bound_in H),m)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32; assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 hence (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 by A99, A109, A114, A115, FUNCT_7:128; ::_thesis: verum end; then Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H) by A112, ZF_LANG1:75; then consider m9 being Element of Union L such that A116: ( m9 in L . a2 & Union L,f9 / ((bound_in H),m9) |= 'not' (the_scope_of H) ) by A109, A107, A108; now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_ (f_/_((bound_in_H),m9))_._x1_=_(f9_/_((bound_in_H),m9))_._x1 let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 ) A117: (f / ((bound_in H),m9)) . (bound_in H) = m9 by FUNCT_7:128; A118: ( x1 <> bound_in H implies ( (f / ((bound_in H),m9)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m9)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32; assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 hence (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 by A99, A109, A107, A117, A118, FUNCT_7:128; ::_thesis: verum end; then A119: a1 c= a2 by A75, A76, A116, ZF_LANG1:75; a2 c= a1 by A109, A106, A111, A112, A113, ZF_LANG1:75; hence a1 = a2 by A119, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_(_(_for_m_being_Element_of_Union_L_holds_not_Union_L,f_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H)_)_implies_a1_=_a2_) assume A120: for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: a1 = a2 now__::_thesis:_for_m_being_Element_of_Union_L_holds_not_Union_L,((Union_L)_!_v)_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H) let m be Element of Union L; ::_thesis: not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H) now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_ (f_/_((bound_in_H),m))_._x1_=_(((Union_L)_!_v)_/_((bound_in_H),m))_._x1 let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 ) A121: (f / ((bound_in H),m)) . (bound_in H) = m by FUNCT_7:128; A122: ( x1 <> bound_in H implies ( (f / ((bound_in H),m)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32; assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 hence (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 by A99, A109, A121, A122, FUNCT_7:128; ::_thesis: verum end; hence not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H) by A120, ZF_LANG1:75; ::_thesis: verum end; hence a1 = a2 by A77, A109, A107, A108, A120; ::_thesis: verum end; then B in rho .: (Funcs (VAR,(L . c))) by A15, A72, A73, A74, A76, A103, A104, A110, FUNCT_1:def_6; then B in si . c by A96, ORDINAL2:19; then B in sup (si | a) by A98, ORDINAL1:10; hence A in sup (si | a) by A69, ORDINAL1:12; ::_thesis: verum end; A123: 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 S4[b] ) holds S4[a] proof let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds S4[b] ) implies S4[a] ) assume that A124: ( a <> 0-element_of W & a is limit_ordinal ) and A125: for b being Ordinal of W st b in a holds si . b c= ksi . b ; ::_thesis: S4[a] thus si . a c= ksi . a ::_thesis: verum proof A126: si . a c= sup (si | a) by A64, A124; let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in si . a or A in ksi . a ) assume A in si . a ; ::_thesis: A in ksi . a then consider B being Ordinal such that A127: B in rng (si | a) and A128: A c= B by A126, ORDINAL2:21; consider x being set such that A129: x in dom (si | a) and A130: B = (si | a) . x by A127, FUNCT_1:def_3; reconsider x = x as Ordinal by A129; A131: a in On W by ORDINAL1:def_9; x in dom si by A129, RELAT_1:57; then x in On W ; then reconsider x = x as Ordinal of W by ORDINAL1:def_9; A132: si . x = B by A129, A130, FUNCT_1:47; A133: si . x c= ksi . x by A125, A129; dom ksi = On W by FUNCT_2:def_1; then ksi . x in ksi . a by A29, A129, A131, ORDINAL2:def_12; hence A in ksi . a by A128, A132, A133, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum end; end; A134: for a being Ordinal of W st S4[a] holds S4[ succ a] proof let a be Ordinal of W; ::_thesis: ( S4[a] implies S4[ succ a] ) assume si . a c= ksi . a ; ::_thesis: S4[ succ a] ( ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) & (si . (succ a)) \/ (ksi . a) in succ ((si . (succ a)) \/ (ksi . a)) ) by A24, ORDINAL1:6; then si . (succ a) in ksi . (succ a) by ORDINAL1:12, XBOOLE_1:7; hence si . (succ a) c= ksi . (succ a) by ORDINAL1:def_2; ::_thesis: verum end; A135: S4[ 0-element_of W] by A23; A136: for a being Ordinal of W holds S4[a] from ZF_REFLE:sch_4(A135, A134, A123); A137: now__::_thesis:_(_bound_in_H_in_Free_(the_scope_of_H)_implies_S1[H]_) assume bound_in H in Free (the_scope_of H) ; ::_thesis: S1[H] thus S1[H] ::_thesis: verum proof take gamma = phi * ksi; ::_thesis: ( gamma is increasing & gamma is continuous & ( for a being Ordinal of W st gamma . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) ex f being Ordinal-Sequence st ( f = phi * ksi & f is increasing ) by A26, A29, ORDINAL4:13; hence ( gamma is increasing & gamma is continuous ) by A27, A29, A46, ORDINAL4:17; ::_thesis: for a being Ordinal of W st gamma . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let a be Ordinal of W; ::_thesis: ( gamma . a = a & {} <> a implies for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) assume that A138: gamma . a = a and A139: {} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H ) a in dom gamma by ORDINAL4:34; then A140: phi . (ksi . a) = gamma . a by FUNCT_1:12; a in dom ksi by ORDINAL4:34; then A141: a c= ksi . a by A29, ORDINAL4:10; ksi . a in dom phi by ORDINAL4:34; then A142: ksi . a c= phi . (ksi . a) by A26, ORDINAL4:10; then A143: ksi . a = a by A138, A141, A140, XBOOLE_0:def_10; A144: phi . a = a by A138, A142, A141, A140, XBOOLE_0:def_10; thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H ) proof assume A145: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H now__::_thesis:_for_g_being_Function_of_VAR,(L_._a)_st_(_for_k_being_Variable_st_g_._k_<>_f_._k_holds_ bound_in_H_=_k_)_holds_ L_._a,g_|=_the_scope_of_H let g be Function of VAR,(L . a); ::_thesis: ( ( for k being Variable st g . k <> f . k holds bound_in H = k ) implies L . a,g |= the_scope_of H ) assume A146: for k being Variable st g . k <> f . k holds bound_in H = k ; ::_thesis: L . a,g |= the_scope_of H now__::_thesis:_for_k_being_Variable_st_((Union_L)_!_g)_._k_<>_((Union_L)_!_f)_._k_holds_ bound_in_H_=_k let k be Variable; ::_thesis: ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k ) ( (Union L) ! f = f & (Union L) ! g = g ) by Th16, ZF_LANG1:def_1; hence ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k ) by A146; ::_thesis: verum end; then Union L,(Union L) ! g |= the_scope_of H by A7, A145, ZF_MODEL:16; hence L . a,g |= the_scope_of H by A28, A139, A144; ::_thesis: verum end; hence L . a,f |= H by A7, ZF_MODEL:16; ::_thesis: verum end; assume that A147: L . a,f |= H and A148: not Union L,(Union L) ! f |= H ; ::_thesis: contradiction consider m being Element of Union L such that A149: not Union L,((Union L) ! f) / ((bound_in H),m) |= the_scope_of H by A7, A148, ZF_LANG1:71; A150: si . a c= ksi . a by A136; A151: si . a = sup (rho .: (Funcs (VAR,(L . a)))) by A22; reconsider h = (Union L) ! f as Element of Funcs (VAR,(Union L)) by FUNCT_2:8; consider a1 being Ordinal of W such that A152: a1 = rho . h and A153: ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and for b being Ordinal of W st ex f being Function of VAR,(Union L) st ( h = f & ( ex m being Element of Union L st ( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds a1 c= b by A16; A154: (Union L) ! f = f by Th16, ZF_LANG1:def_1; Union L,((Union L) ! f) / ((bound_in H),m) |= 'not' (the_scope_of H) by A149, ZF_MODEL:14; then consider m being Element of Union L such that A155: m in L . a1 and A156: Union L,((Union L) ! f) / ((bound_in H),m) |= 'not' (the_scope_of H) by A153; f in Funcs (VAR,(L . a)) by FUNCT_2:8; then a1 in rho .: (Funcs (VAR,(L . a))) by A15, A152, A154, FUNCT_1:def_6; then a1 in si . a by A151, ORDINAL2:19; then L . a1 c= L . a by A2, A143, A150; then reconsider m9 = m as Element of L . a by A155; ((Union L) ! f) / ((bound_in H),m) = (Union L) ! (f / ((bound_in H),m9)) by A154, Th16, ZF_LANG1:def_1; then not Union L,(Union L) ! (f / ((bound_in H),m9)) |= the_scope_of H by A156, ZF_MODEL:14; then not L . a,f / ((bound_in H),m9) |= the_scope_of H by A28, A139, A144; hence contradiction by A7, A147, ZF_LANG1:71; ::_thesis: verum end; end; now__::_thesis:_(_not_bound_in_H_in_Free_(the_scope_of_H)_implies_S1[H]_) assume A157: not bound_in H in Free (the_scope_of H) ; ::_thesis: S1[H] thus S1[H] ::_thesis: verum proof take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) thus ( phi is increasing & phi is continuous ) by A26, A27; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) assume A158: ( phi . a = a & {} <> a ) ; ::_thesis: for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H ) thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H ) proof A159: for k being Variable st ((Union L) ! f) . k <> ((Union L) ! f) . k holds bound_in H = k ; assume Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H then Union L,(Union L) ! f |= the_scope_of H by A7, A159, ZF_MODEL:16; then L . a,f |= the_scope_of H by A28, A158; hence L . a,f |= H by A7, A157, ZFMODEL1:10; ::_thesis: verum end; A160: for k being Variable st f . k <> f . k holds bound_in H = k ; assume L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H then L . a,f |= the_scope_of H by A7, A160, ZF_MODEL:16; then Union L,(Union L) ! f |= the_scope_of H by A28, A158; hence Union L,(Union L) ! f |= H by A7, A157, ZFMODEL1:10; ::_thesis: verum end; end; hence S1[H] by A137; ::_thesis: verum end; A161: for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] ) assume H is conjunctive ; ::_thesis: ( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] ) then A162: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40; given fi1 being Ordinal-Sequence of W such that A163: fi1 is increasing and A164: fi1 is continuous and A165: for a being Ordinal of W st fi1 . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= the_left_argument_of H iff L . a,f |= the_left_argument_of H ) ; ::_thesis: ( not S1[ the_right_argument_of H] or S1[H] ) given fi2 being Ordinal-Sequence of W such that A166: fi2 is increasing and A167: fi2 is continuous and A168: for a being Ordinal of W st fi2 . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= the_right_argument_of H iff L . a,f |= the_right_argument_of H ) ; ::_thesis: S1[H] take phi = fi2 * fi1; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) ex fi being Ordinal-Sequence st ( fi = fi2 * fi1 & fi is increasing ) by A163, A166, ORDINAL4:13; hence ( phi is increasing & phi is continuous ) by A163, A164, A167, ORDINAL4:17; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) assume that A169: phi . a = a and A170: {} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) a in dom fi1 by ORDINAL4:34; then A171: a c= fi1 . a by A163, ORDINAL4:10; let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H ) A172: a in dom phi by ORDINAL4:34; A173: a in dom fi2 by ORDINAL4:34; A174: now__::_thesis:_not_fi1_._a_<>_a assume fi1 . a <> a ; ::_thesis: contradiction then a c< fi1 . a by A171, XBOOLE_0:def_8; then A175: a in fi1 . a by ORDINAL1:11; A176: phi . a = fi2 . (fi1 . a) by A172, FUNCT_1:12; fi1 . a in dom fi2 by ORDINAL4:34; then fi2 . a in fi2 . (fi1 . a) by A166, A175, ORDINAL2:def_12; hence contradiction by A166, A169, A173, A176, ORDINAL1:5, ORDINAL4:10; ::_thesis: verum end; then A177: fi2 . a = a by A169, A172, FUNCT_1:12; thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H ) proof assume A178: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H then Union L,(Union L) ! f |= the_right_argument_of H by A162, ZF_MODEL:15; then A179: L . a,f |= the_right_argument_of H by A168, A170, A177; Union L,(Union L) ! f |= the_left_argument_of H by A162, A178, ZF_MODEL:15; then L . a,f |= the_left_argument_of H by A165, A170, A174; hence L . a,f |= H by A162, A179, ZF_MODEL:15; ::_thesis: verum end; assume A180: L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H then L . a,f |= the_right_argument_of H by A162, ZF_MODEL:15; then A181: Union L,(Union L) ! f |= the_right_argument_of H by A168, A170, A177; L . a,f |= the_left_argument_of H by A162, A180, ZF_MODEL:15; then Union L,(Union L) ! f |= the_left_argument_of H by A165, A170, A174; hence Union L,(Union L) ! f |= H by A162, A181, ZF_MODEL:15; ::_thesis: verum end; A182: for H being ZF-formula st H is atomic holds S1[H] proof A183: dom (id (On W)) = On W ; then reconsider phi = id (On W) as T-Sequence by ORDINAL1:def_7; A184: rng (id (On W)) = On W ; reconsider phi = phi as Ordinal-Sequence ; reconsider phi = phi as Ordinal-Sequence of W by A183, A184, FUNCT_2:def_1, RELSET_1:4; let H be ZF-formula; ::_thesis: ( H is atomic implies S1[H] ) assume A185: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S1[H] take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) thus A186: phi is increasing ::_thesis: ( phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) proof let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds ( not A in b1 or not b1 in dom phi or phi . A in phi . b1 ) let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B ) assume A187: ( A in B & B in dom phi ) ; ::_thesis: phi . A in phi . B then phi . A = A by FUNCT_1:18, ORDINAL1:10; hence phi . A in phi . B by A187, FUNCT_1:18; ::_thesis: verum end; thus phi is continuous ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) proof let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds ( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A ) let B be Ordinal; ::_thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A ) assume that A188: A in dom phi and A189: ( A <> {} & A is limit_ordinal ) and A190: B = phi . A ; ::_thesis: B is_limes_of phi | A A191: A c= dom phi by A188, ORDINAL1:def_2; phi | A = phi * (id A) by RELAT_1:65 .= id ((dom phi) /\ A) by A183, FUNCT_1:22 .= id A by A191, XBOOLE_1:28 ; then A192: rng (phi | A) = A by RELAT_1:45; phi . A = A by A188, FUNCT_1:18; then A193: sup (phi | A) = B by A190, A192, ORDINAL2:18; A194: phi | A is increasing by A186, ORDINAL4:15; dom (phi | A) = A by A191, RELAT_1:62; hence B is_limes_of phi | A by A189, A193, A194, ORDINAL4:8; ::_thesis: verum end; let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) assume that phi . a = a and {} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H ) thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H ) proof assume A195: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H A196: (Union L) ! f = f by Th16, ZF_LANG1:def_1; A197: now__::_thesis:_(_H_is_being_membership_implies_L_._a,f_|=_H_) assume H is being_membership ; ::_thesis: L . a,f |= H then A198: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37; then ((Union L) ! f) . (Var1 H) in ((Union L) ! f) . (Var2 H) by A195, ZF_MODEL:13; hence L . a,f |= H by A196, A198, ZF_MODEL:13; ::_thesis: verum end; now__::_thesis:_(_H_is_being_equality_implies_L_._a,f_|=_H_) assume H is being_equality ; ::_thesis: L . a,f |= H then A199: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36; then ((Union L) ! f) . (Var1 H) = ((Union L) ! f) . (Var2 H) by A195, ZF_MODEL:12; hence L . a,f |= H by A196, A199, ZF_MODEL:12; ::_thesis: verum end; hence L . a,f |= H by A185, A197; ::_thesis: verum end; assume A200: L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H A201: (Union L) ! f = f by Th16, ZF_LANG1:def_1; A202: now__::_thesis:_(_H_is_being_membership_implies_Union_L,(Union_L)_!_f_|=_H_) assume H is being_membership ; ::_thesis: Union L,(Union L) ! f |= H then A203: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37; then f . (Var1 H) in f . (Var2 H) by A200, ZF_MODEL:13; hence Union L,(Union L) ! f |= H by A201, A203, ZF_MODEL:13; ::_thesis: verum end; now__::_thesis:_(_H_is_being_equality_implies_Union_L,(Union_L)_!_f_|=_H_) assume H is being_equality ; ::_thesis: Union L,(Union L) ! f |= H then A204: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36; then f . (Var1 H) = f . (Var2 H) by A200, ZF_MODEL:12; hence Union L,(Union L) ! f |= H by A201, A204, ZF_MODEL:12; ::_thesis: verum end; hence Union L,(Union L) ! f |= H by A185, A202; ::_thesis: verum end; A205: for H being ZF-formula st H is negative & S1[ the_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is negative & S1[ the_argument_of H] implies S1[H] ) assume H is negative ; ::_thesis: ( not S1[ the_argument_of H] or S1[H] ) then A206: H = 'not' (the_argument_of H) by ZF_LANG:def_30; given phi being Ordinal-Sequence of W such that A207: ( phi is increasing & phi is continuous ) and A208: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= the_argument_of H iff L . a,f |= the_argument_of H ) ; ::_thesis: S1[H] take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) thus ( phi is increasing & phi is continuous ) by A207; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) assume A209: ( phi . a = a & {} <> a ) ; ::_thesis: for f being Function of VAR,(L . a) holds ( Union L,(Union L) ! f |= H iff L . a,f |= H ) let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H ) thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H ) proof assume Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H then not Union L,(Union L) ! f |= the_argument_of H by A206, ZF_MODEL:14; then not L . a,f |= the_argument_of H by A208, A209; hence L . a,f |= H by A206, ZF_MODEL:14; ::_thesis: verum end; assume L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H then not L . a,f |= the_argument_of H by A206, ZF_MODEL:14; then not Union L,(Union L) ! f |= the_argument_of H by A208, A209; hence Union L,(Union L) ! f |= H by A206, ZF_MODEL:14; ::_thesis: verum end; thus for H being ZF-formula holds S1[H] from ZF_LANG:sch_1(A182, A205, A161, A6); ::_thesis: verum end; begin theorem :: ZF_REFLE:21 for M being non countable Aleph st M is strongly_inaccessible holds Rank M is being_a_model_of_ZF proof let M be non countable Aleph; ::_thesis: ( M is strongly_inaccessible implies Rank M is being_a_model_of_ZF ) assume M is strongly_inaccessible ; ::_thesis: Rank M is being_a_model_of_ZF then A1: Rank M is Universe by CARD_LAR:38; omega c= M ; then omega c< M by XBOOLE_0:def_8; then A2: omega in M by ORDINAL1:11; M c= Rank M by CLASSES1:38; hence Rank M is being_a_model_of_ZF by A1, A2, Th6; ::_thesis: verum end;