:: ZF_FUND2 semantic presentation begin definition let H be ZF-formula; let M be non empty set ; let v be Function of VAR,M; func Section (H,v) -> Subset of M equals :Def1: :: ZF_FUND2:def 1 { m where m is Element of M : M,v / ((x. 0),m) |= H } if x. 0 in Free H otherwise {} ; coherence ( ( x. 0 in Free H implies { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ) & ( not x. 0 in Free H implies {} is Subset of M ) ) proof thus ( x. 0 in Free H implies { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ) ::_thesis: ( not x. 0 in Free H implies {} is Subset of M ) proof set X = { m where m is Element of M : M,v / ((x. 0),m) |= H } ; assume x. 0 in Free H ; ::_thesis: { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M { m where m is Element of M : M,v / ((x. 0),m) |= H } c= M proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { m where m is Element of M : M,v / ((x. 0),m) |= H } or u in M ) assume u in { m where m is Element of M : M,v / ((x. 0),m) |= H } ; ::_thesis: u in M then ex m being Element of M st ( u = m & M,v / ((x. 0),m) |= H ) ; hence u in M ; ::_thesis: verum end; hence { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ; ::_thesis: verum end; thus ( not x. 0 in Free H implies {} is Subset of M ) by XBOOLE_1:2; ::_thesis: verum end; consistency for b1 being Subset of M holds verum ; end; :: deftheorem Def1 defines Section ZF_FUND2:def_1_:_ for H being ZF-formula for M being non empty set for v being Function of VAR,M holds ( ( x. 0 in Free H implies Section (H,v) = { m where m is Element of M : M,v / ((x. 0),m) |= H } ) & ( not x. 0 in Free H implies Section (H,v) = {} ) ); definition let M be non empty set ; attrM is predicatively_closed means :Def2: :: ZF_FUND2:def 2 for H being ZF-formula for E being non empty set for f being Function of VAR,E st E in M holds Section (H,f) in M; end; :: deftheorem Def2 defines predicatively_closed ZF_FUND2:def_2_:_ for M being non empty set holds ( M is predicatively_closed iff for H being ZF-formula for E being non empty set for f being Function of VAR,E st E in M holds Section (H,f) in M ); theorem Th1: :: ZF_FUND2:1 for E being non empty set for e being Element of E for f being Function of VAR,E st E is epsilon-transitive holds Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) proof let E be non empty set ; ::_thesis: for e being Element of E for f being Function of VAR,E st E is epsilon-transitive holds Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) let e be Element of E; ::_thesis: for f being Function of VAR,E st E is epsilon-transitive holds Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) let f be Function of VAR,E; ::_thesis: ( E is epsilon-transitive implies Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) ) set H = All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))); set v = f / ((x. 1),e); set S = Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))); Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) = (Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:62 .= ((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:64 .= ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59 .= ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59 .= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) by XBOOLE_1:42 .= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76 .= {(x. 0)} \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76 .= {(x. 0),(x. 1)} by ENUMSET1:1 ; then x. 0 in Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) by TARSKI:def_2; then A1: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = { m where m is Element of E : E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) } by Def1; assume A2: for X being set st X in E holds X c= E ; :: according to ORDINAL1:def_2 ::_thesis: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) thus Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) c= E /\ (bool e) :: according to XBOOLE_0:def_10 ::_thesis: E /\ (bool e) c= Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) or u in E /\ (bool e) ) assume u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) ; ::_thesis: u in E /\ (bool e) then consider m being Element of E such that A3: u = m and A4: E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by A1; A5: m c= E by A2; m c= e proof let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in m or u1 in e ) assume A6: u1 in m ; ::_thesis: u1 in e then reconsider u1 = u1 as Element of E by A5; A7: (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 2) = u1 by FUNCT_7:128; A8: E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by A4, ZF_LANG1:71; A9: ( (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76; ( m = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; then E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 0) by A6, A7, ZF_MODEL:13; then ( (f / ((x. 1),e)) . (x. 1) = e & E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 1) ) by A8, FUNCT_7:128, ZF_MODEL:18; hence u1 in e by A7, A9, ZF_MODEL:13; ::_thesis: verum end; then u in bool e by A3, ZFMISC_1:def_1; hence u in E /\ (bool e) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in E /\ (bool e) or u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) ) assume A10: u in E /\ (bool e) ; ::_thesis: u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) then A11: u in bool e by XBOOLE_0:def_4; reconsider u = u as Element of E by A10, XBOOLE_0:def_4; now__::_thesis:_for_m_being_Element_of_E_holds_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_((x._2)_'in'_(x._0))_=>_((x._2)_'in'_(x._1)) A12: (f / ((x. 1),e)) . (x. 1) = e by FUNCT_7:128; let m be Element of E; ::_thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) A13: (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 2) = m by FUNCT_7:128; A14: ( u = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; A15: ( (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76; now__::_thesis:_(_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_(x._2)_'in'_(x._0)_implies_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_(x._2)_'in'_(x._1)_) assume E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 0) ; ::_thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) then m in u by A13, A14, ZF_MODEL:13; hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) by A11, A13, A15, A12, ZF_MODEL:13; ::_thesis: verum end; hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by ZF_MODEL:18; ::_thesis: verum end; then E,(f / ((x. 1),e)) / ((x. 0),u) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by ZF_LANG1:71; hence u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) by A1; ::_thesis: verum end; Lm1: for g being Function for u1 being set st u1 in Union g holds ex u2 being set st ( u2 in dom g & u1 in g . u2 ) proof let g be Function; ::_thesis: for u1 being set st u1 in Union g holds ex u2 being set st ( u2 in dom g & u1 in g . u2 ) let u1 be set ; ::_thesis: ( u1 in Union g implies ex u2 being set st ( u2 in dom g & u1 in g . u2 ) ) assume u1 in Union g ; ::_thesis: ex u2 being set st ( u2 in dom g & u1 in g . u2 ) then u1 in union (rng g) by CARD_3:def_4; then consider X being set such that A1: u1 in X and A2: X in rng g by TARSKI:def_4; consider u2 being set such that A3: ( u2 in dom g & X = g . u2 ) by A2, FUNCT_1:def_3; take u2 ; ::_thesis: ( u2 in dom g & u1 in g . u2 ) thus ( u2 in dom g & u1 in g . u2 ) by A1, A3; ::_thesis: verum end; theorem Th2: :: ZF_FUND2:2 for W being Universe for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds Union L |= the_axiom_of_power_sets proof let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds Union L |= the_axiom_of_power_sets let L be DOMAIN-Sequence of W; ::_thesis: ( ( for a, b being Ordinal of W st a in b holds L . a c= L . b ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies Union L |= the_axiom_of_power_sets ) assume that A1: for a, b being Ordinal of W st a in b holds L . a c= L . b and A2: for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) and A3: Union L is predicatively_closed ; ::_thesis: Union L |= the_axiom_of_power_sets set M = Union L; A4: for X being set for a being Ordinal of W st X in L . a holds (L . a) /\ (bool X) in Union L proof let X be set ; ::_thesis: for a being Ordinal of W st X in L . a holds (L . a) /\ (bool X) in Union L let a be Ordinal of W; ::_thesis: ( X in L . a implies (L . a) /\ (bool X) in Union L ) set f = the Function of VAR,(L . a); assume X in L . a ; ::_thesis: (L . a) /\ (bool X) in Union L then reconsider e = X as Element of L . a ; L . a in Union L by A2; then A5: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),( the Function of VAR,(L . a) / ((x. 1),e))) in Union L by A3, Def2; L . a is epsilon-transitive by A2; hence (L . a) /\ (bool X) in Union L by A5, Th1; ::_thesis: verum end; A6: now__::_thesis:_for_X_being_set_st_X_in_Union_L_holds_ (Union_L)_/\_(bool_X)_in_Union_L defpred S1[ set , set ] means $1 in L . $2; let X be set ; ::_thesis: ( X in Union L implies (Union L) /\ (bool X) in Union L ) assume A7: X in Union L ; ::_thesis: (Union L) /\ (bool X) in Union L A8: X in bool X by ZFMISC_1:def_1; then reconsider D = (Union L) /\ (bool X) as non empty set by A7, XBOOLE_0:def_4; A9: X in (Union L) /\ (bool X) by A7, A8, XBOOLE_0:def_4; A10: for d being Element of D ex a being Ordinal of W st S1[d,a] proof let d be Element of D; ::_thesis: ex a being Ordinal of W st S1[d,a] d in Union L by XBOOLE_0:def_4; then consider u2 being set such that A11: u2 in dom L and A12: d in L . u2 by Lm1; u2 in On W by A11, ZF_REFLE:def_2; then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7; take u2 ; ::_thesis: S1[d,u2] thus S1[d,u2] by A12; ::_thesis: verum end; consider f being Function such that A13: ( dom f = D & ( for d being Element of D ex a being Ordinal of W st ( a = f . d & S1[d,a] & ( for b being Ordinal of W st S1[d,b] holds a c= b ) ) ) ) from ZF_REFLE:sch_1(A10); A14: rng f c= W proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng f or u in W ) assume u in rng f ; ::_thesis: u in W then consider u1 being set such that A15: u1 in D and A16: u = f . u1 by A13, FUNCT_1:def_3; reconsider u1 = u1 as Element of D by A15; ex a being Ordinal of W st ( a = f . u1 & u1 in L . a & ( for b being Ordinal of W st u1 in L . b holds a c= b ) ) by A13; hence u in W by A16; ::_thesis: verum end; A17: (Union L) /\ (bool X) c= bool X by XBOOLE_1:17; bool X in W by A7, CLASSES2:59; then D in W by A17, CLASSES1:def_1; then ( rng f = f .: (dom f) & card D in card W ) by CLASSES2:1, RELAT_1:113; then card (rng f) in card W by A13, CARD_1:67, ORDINAL1:12; then rng f in W by A14, CLASSES1:1; then reconsider a = sup (rng f) as Ordinal of W by ZF_REFLE:19; A18: D c= L . a proof let u2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u2 in D or u2 in L . a ) assume u2 in D ; ::_thesis: u2 in L . a then reconsider d = u2 as Element of D ; consider c being Ordinal of W such that A19: c = f . d and A20: d in L . c and for b being Ordinal of W st d in L . b holds c c= b by A13; c in rng f by A13, A19, FUNCT_1:def_3; then L . c c= L . a by A1, ORDINAL2:19; hence u2 in L . a by A20; ::_thesis: verum end; A21: (L . a) /\ (bool X) c= D by XBOOLE_1:26, ZF_REFLE:16; D /\ (bool X) = (Union L) /\ ((bool X) /\ (bool X)) by XBOOLE_1:16; then D c= (L . a) /\ (bool X) by A18, XBOOLE_1:26; then D = (L . a) /\ (bool X) by A21, XBOOLE_0:def_10; hence (Union L) /\ (bool X) in Union L by A4, A9, A18; ::_thesis: verum end; Union L is epsilon-transitive proof let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L ) assume X in Union L ; ::_thesis: X c= Union L then consider u being set such that A22: u in dom L and A23: X in L . u by Lm1; reconsider u = u as Ordinal by A22; u in On W by A22, ZF_REFLE:def_2; then reconsider u = u as Ordinal of W by ZF_REFLE:7; L . u is epsilon-transitive by A2; then A24: X c= L . u by A23, ORDINAL1:def_2; let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L ) A25: L . u c= Union L by ZF_REFLE:16; assume u1 in X ; ::_thesis: u1 in Union L then u1 in L . u by A24; hence u1 in Union L by A25; ::_thesis: verum end; hence Union L |= the_axiom_of_power_sets by A6, ZFMODEL1:9; ::_thesis: verum end; Lm2: for H being ZF-formula for M being non empty set for v being Function of VAR,M for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) proof let H be ZF-formula; ::_thesis: for M being non empty set for v being Function of VAR,M for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) let M be non empty set ; ::_thesis: for v being Function of VAR,M for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) let v be Function of VAR,M; ::_thesis: for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) let x be Variable; ::_thesis: ( not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) ) assume that A1: not x in variables_in H and A2: {(x. 0),(x. 1),(x. 2)} misses Free H and A3: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1; then A4: not x. 0 in Free H by A2, XBOOLE_0:3; hence {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) by A1, A2, ZFMODEL2:2; ::_thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) A5: not x. 0 in Free (H / ((x. 0),x)) by A1, A4, ZFMODEL2:2; A6: now__::_thesis:_for_m3_being_Element_of_M_ex_m0_being_Element_of_M_st_ for_m4_being_Element_of_M_holds_ (_(_M,(v_/_((x._3),m3))_/_((x._4),m4)_|=_H_/_((x._0),x)_implies_m4_=_m0_)_&_(_m4_=_m0_implies_M,(v_/_((x._3),m3))_/_((x._4),m4)_|=_H_/_((x._0),x)_)_) let m3 be Element of M; ::_thesis: ex m0 being Element of M st for m4 being Element of M holds ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) ) consider m0 being Element of M such that A7: for m being Element of M holds ( M,(v / ((x. 3),m3)) / ((x. 4),m) |= H iff m = m0 ) by A3, A4, ZFMODEL2:19; take m0 = m0; ::_thesis: for m4 being Element of M holds ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) ) let m4 be Element of M; ::_thesis: ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) ) thus ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) ::_thesis: ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) proof assume M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ; ::_thesis: m4 = m0 then M,((v / ((x. 3),m3)) / ((x. 4),m4)) / ((x. 0),(((v / ((x. 3),m3)) / ((x. 4),m4)) . x)) |= H by A1, ZFMODEL2:12; then M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H by A4, ZFMODEL2:9; hence m4 = m0 by A7; ::_thesis: verum end; assume m4 = m0 ; ::_thesis: M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) then M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H by A7; then M,((v / ((x. 3),m3)) / ((x. 4),m4)) / ((x. 0),(((v / ((x. 3),m3)) / ((x. 4),m4)) . x)) |= H by A4, ZFMODEL2:9; hence M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) by A1, ZFMODEL2:12; ::_thesis: verum end; Free H = Free (H / ((x. 0),x)) by A1, A4, ZFMODEL2:2; hence A8: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) by A4, A6, ZFMODEL2:19; ::_thesis: def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) now__::_thesis:_for_u_being_set_st_u_in_M_holds_ (def_func'_(H,v))_._u_=_(def_func'_((H_/_((x._0),x)),v))_._u let u be set ; ::_thesis: ( u in M implies (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u ) assume u in M ; ::_thesis: (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u then reconsider u9 = u as Element of M ; set m = (def_func' (H,v)) . u9; M,(v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9)) |= H by A3, A4, ZFMODEL2:10; then M,((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) / ((x. 0),(((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) . x)) |= H by A4, ZFMODEL2:9; then M,(v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9)) |= H / ((x. 0),x) by A1, ZFMODEL2:12; hence (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u by A5, A8, ZFMODEL2:10; ::_thesis: verum end; hence def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) by FUNCT_2:12; ::_thesis: verum end; Lm3: for H being ZF-formula for M being non empty set for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds for m being Element of M holds (def_func' (H,v)) .: m = {} proof let H be ZF-formula; ::_thesis: for M being non empty set for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds for m being Element of M holds (def_func' (H,v)) .: m = {} let M be non empty set ; ::_thesis: for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds for m being Element of M holds (def_func' (H,v)) .: m = {} let v be Function of VAR,M; ::_thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H implies for m being Element of M holds (def_func' (H,v)) .: m = {} ) set m3 = the Element of M; assume that A1: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and A2: not x. 4 in Free H ; ::_thesis: for m being Element of M holds (def_func' (H,v)) .: m = {} M,v / ((x. 3), the Element of M) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A1, ZF_LANG1:71; then consider m0 being Element of M such that A3: M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73; let m be Element of M; ::_thesis: (def_func' (H,v)) .: m = {} set u = the Element of (def_func' (H,v)) .: m; assume (def_func' (H,v)) .: m <> {} ; ::_thesis: contradiction then consider u1 being set such that A4: u1 in dom (def_func' (H,v)) and A5: u1 in m and the Element of (def_func' (H,v)) .: m = (def_func' (H,v)) . u1 by FUNCT_1:def_6; set f = (v / ((x. 3), the Element of M)) / ((x. 0),m0); reconsider u1 = u1 as Element of M by A4; A6: now__::_thesis:_for_m4_being_Element_of_M_holds_ (_M,(v_/_((x._3),_the_Element_of_M))_/_((x._0),m0)_|=_H_iff_m4_=_m0_) let m4 be Element of M; ::_thesis: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 ) M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71; then ( M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H iff M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ) by ZF_MODEL:19; then A7: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 0) ) by A2, ZFMODEL2:9, ZF_MODEL:12; ( (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = m4 & ((v / ((x. 3), the Element of M)) / ((x. 0),m0)) . (x. 0) = m0 ) by FUNCT_7:128; hence ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 ) by A7, FUNCT_7:32, ZF_LANG1:76; ::_thesis: verum end; then M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H ; then ( u1 = m0 & m = m0 ) by A6; hence contradiction by A5; ::_thesis: verum end; Lm4: for H being ZF-formula for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) proof let H be ZF-formula; ::_thesis: for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) let y, x be Variable; ::_thesis: ( not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 implies ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) ) A1: x. 0 <> x. 3 by ZF_LANG1:76; assume that A2: not y in variables_in H and A3: x <> x. 0 and A4: y <> x. 0 and A5: y <> x. 4 ; ::_thesis: ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) set G = (H / ((x. 0),y)) / ((x. 4),(x. 0)); A6: Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) = (Free (((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:66 .= ((Free ((x. 3) 'in' x)) \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:61 .= ({(x. 3),x} \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:59 .= ({(x. 3),x} \ {(x. 3)}) \/ ((Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)}) by XBOOLE_1:42 ; A7: x. 0 <> x. 4 by ZF_LANG1:76; A8: now__::_thesis:_(_x._4_in_Free_H_implies_x._0_in_Free_(Ex_((x._3),(((x._3)_'in'_x)_'&'_((H_/_((x._0),y))_/_((x._4),(x._0))))))_) assume A9: x. 4 in Free H ; ::_thesis: x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) A10: x. 4 in Free (H / ((x. 0),y)) proof now__::_thesis:_x._4_in_Free_(H_/_((x._0),y)) percases ( x. 0 in Free H or not x. 0 in Free H ) ; supposeA11: x. 0 in Free H ; ::_thesis: x. 4 in Free (H / ((x. 0),y)) not x. 4 in {(x. 0)} by A7, TARSKI:def_1; then A12: x. 4 in (Free H) \ {(x. 0)} by A9, XBOOLE_0:def_5; Free (H / ((x. 0),y)) = ((Free H) \ {(x. 0)}) \/ {y} by A2, A11, ZFMODEL2:2; hence x. 4 in Free (H / ((x. 0),y)) by A12, XBOOLE_0:def_3; ::_thesis: verum end; suppose not x. 0 in Free H ; ::_thesis: x. 4 in Free (H / ((x. 0),y)) hence x. 4 in Free (H / ((x. 0),y)) by A2, A9, ZFMODEL2:2; ::_thesis: verum end; end; end; hence x. 4 in Free (H / ((x. 0),y)) ; ::_thesis: verum end; A13: x. 0 in {(x. 0)} by TARSKI:def_1; not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184; then Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) = ((Free (H / ((x. 0),y))) \ {(x. 4)}) \/ {(x. 0)} by A10, ZFMODEL2:2; then A14: x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) by A13, XBOOLE_0:def_3; not x. 0 in {(x. 3)} by A1, TARSKI:def_1; then x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} by A14, XBOOLE_0:def_5; hence x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) by A6, XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_x._0_in_Free_(Ex_((x._3),(((x._3)_'in'_x)_'&'_((H_/_((x._0),y))_/_((x._4),(x._0))))))_implies_x._4_in_Free_H_) assume x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ; ::_thesis: x. 4 in Free H then ( x. 0 in {(x. 3),x} \ {(x. 3)} or x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} ) by A6, XBOOLE_0:def_3; then A15: ( x. 0 in {(x. 3),x} or x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) ) by XBOOLE_0:def_5; A16: not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184; A17: now__::_thesis:_x._4_in_Free_(H_/_((x._0),y)) assume not x. 4 in Free (H / ((x. 0),y)) ; ::_thesis: contradiction then A18: x. 0 in Free (H / ((x. 0),y)) by A3, A1, A15, A16, TARSKI:def_2, ZFMODEL2:2; Free (H / ((x. 0),y)) c= variables_in (H / ((x. 0),y)) by ZF_LANG1:151; hence contradiction by A4, A18, ZF_LANG1:184; ::_thesis: verum end; Free (H / ((x. 0),y)) c= ((Free H) \ {(x. 0)}) \/ {y} by ZFMODEL2:1; then ( x. 4 in (Free H) \ {(x. 0)} or x. 4 in {y} ) by A17, XBOOLE_0:def_3; hence x. 4 in Free H by A5, TARSKI:def_1, XBOOLE_0:def_5; ::_thesis: verum end; hence ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) by A8; ::_thesis: verum end; theorem Th3: :: ZF_FUND2:3 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for 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) and A4: for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) and A5: Union L is predicatively_closed ; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for H set M = Union L; A6: now__::_thesis:_for_H_being_ZF-formula for_f_being_Function_of_VAR,(Union_L)_st_{(x._0),(x._1),(x._2)}_misses_Free_H_&_Union_L,f_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))_holds_ for_u_being_Element_of_Union_L_holds_(def_func'_(H,f))_.:_u_in_Union_L defpred S1[ set , set ] means $1 in L . $2; let H be ZF-formula; ::_thesis: for f being Function of VAR,(Union L) st {(x. 0),(x. 1),(x. 2)} misses Free H & Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of Union L holds (def_func' (H,f)) .: u in Union L let f be Function of VAR,(Union L); ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of Union L holds (def_func' (H,f)) .: u in Union L ) assume that A7: {(x. 0),(x. 1),(x. 2)} misses Free H and A8: Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for u being Element of Union L holds (def_func' (H,f)) .: u in Union L consider k being Element of NAT such that A9: for i being Element of NAT st x. i in variables_in H holds i < k by ZFMODEL2:3; set p = H / ((x. 0),(x. (k + 5))); k + 0 = k ; then A10: not x. (k + 5) in variables_in H by A9, XREAL_1:7; then A11: ( Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),(x. (k + 5)))) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,f) = def_func' ((H / ((x. 0),(x. (k + 5)))),f) ) by A7, A8, Lm2; set F = def_func' (H,f); A12: for d being Element of Union L ex a being Ordinal of W st S1[d,a] proof let d be Element of Union L; ::_thesis: ex a being Ordinal of W st S1[d,a] consider u being set such that A13: u in dom L and A14: d in L . u by Lm1; u in On W by A13, ZF_REFLE:def_2; then reconsider u = u as Ordinal of W by ZF_REFLE:7; take u ; ::_thesis: S1[d,u] thus S1[d,u] by A14; ::_thesis: verum end; consider g being Function such that A15: ( dom g = Union L & ( for d being Element of Union L ex a being Ordinal of W st ( a = g . d & S1[d,a] & ( for b being Ordinal of W st S1[d,b] holds a c= b ) ) ) ) from ZF_REFLE:sch_1(A12); A16: rng g c= W proof let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in rng g or u1 in W ) assume u1 in rng g ; ::_thesis: u1 in W then consider u2 being set such that A17: u2 in dom g and A18: u1 = g . u2 by FUNCT_1:def_3; reconsider d = u2 as Element of Union L by A15, A17; ex a being Ordinal of W st ( a = g . d & d in L . a & ( for b being Ordinal of W st d in L . b holds a c= b ) ) by A15; hence u1 in W by A18; ::_thesis: verum end; ( card VAR = omega & omega in card W ) by A1, CARD_1:5, CARD_1:47, CLASSES2:1, ZF_REFLE:17; then A19: card (dom f) in card W by FUNCT_2:def_1; rng f = f .: (dom f) by RELAT_1:113; then card (rng f) in card W by A19, CARD_1:67, ORDINAL1:12; then A20: card (g .: (rng f)) in card W by CARD_1:67, ORDINAL1:12; g .: (rng f) c= rng g by RELAT_1:111; then g .: (rng f) c= W by A16, XBOOLE_1:1; then g .: (rng f) in W by A20, CLASSES1:1; then reconsider b2 = sup (g .: (rng f)) as Ordinal of W by ZF_REFLE:19; A21: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1; {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),(x. (k + 5)))) by A7, A8, A10, Lm2; then A22: not x. 0 in Free (H / ((x. 0),(x. (k + 5)))) by A21, XBOOLE_0:3; A23: for X being set for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds X c= L . a proof let X be set ; ::_thesis: for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds X c= L . a let a be Ordinal of W; ::_thesis: ( X c= Union L & sup (g .: X) c= a implies X c= L . a ) assume that A24: X c= Union L and A25: sup (g .: X) c= a ; ::_thesis: X c= L . a let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in L . a ) assume A26: u1 in X ; ::_thesis: u1 in L . a then reconsider d = u1 as Element of Union L by A24; consider b being Ordinal of W such that A27: b = g . d and A28: d in L . b and for a being Ordinal of W st d in L . a holds b c= a by A15; b in g .: X by A15, A26, A27, FUNCT_1:def_6; then b in sup (g .: X) by ORDINAL2:19; then L . b c= L . a by A2, A25; hence u1 in L . a by A28; ::_thesis: verum end; let u be Element of Union L; ::_thesis: (def_func' (H,f)) .: u in Union L consider b0 being Ordinal of W such that b0 = g . u and A29: u in L . b0 and for b being Ordinal of W st u in L . b holds b0 c= b by A15; A30: card u in card W by CLASSES2:1; k + 0 = k ; then A31: ( 0 <= k & k < k + 5 ) by NAT_1:2, XREAL_1:6; then A32: not x. 0 in variables_in (H / ((x. 0),(x. (k + 5)))) by ZF_LANG1:76, ZF_LANG1:184; g .: ((def_func' (H,f)) .: u) c= rng g by RELAT_1:111; then A33: g .: ((def_func' (H,f)) .: u) c= W by A16, XBOOLE_1:1; ( card (g .: ((def_func' (H,f)) .: u)) c= card ((def_func' (H,f)) .: u) & card ((def_func' (H,f)) .: u) c= card u ) by CARD_1:67; then card (g .: ((def_func' (H,f)) .: u)) in card W by A30, ORDINAL1:12, XBOOLE_1:1; then g .: ((def_func' (H,f)) .: u) in W by A33, CLASSES1:1; then reconsider b1 = sup (g .: ((def_func' (H,f)) .: u)) as Ordinal of W by ZF_REFLE:19; set b = b0 \/ b1; set a = (b0 \/ b1) \/ b2; A34: (def_func' (H,f)) .: u c= L . (b0 \/ b1) by A23, XBOOLE_1:7; consider phi being Ordinal-Sequence of W such that A35: ( phi is increasing & phi is continuous ) and A36: for a being Ordinal of W st phi . a = a & {} <> a holds for v being Function of VAR,(L . a) holds ( Union L,(Union L) ! v |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) iff L . a,v |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) ) by A1, A2, A3, ZF_REFLE:20; consider a1 being Ordinal of W such that A37: (b0 \/ b1) \/ b2 in a1 and A38: phi . a1 = a1 by A1, A35, ZFREFLE1:28; A39: rng f c= L . a1 proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng f or u in L . a1 ) A40: b2 c= (b0 \/ b1) \/ b2 by XBOOLE_1:7; assume A41: u in rng f ; ::_thesis: u in L . a1 then consider u1 being set such that A42: u1 in dom f and A43: u = f . u1 by FUNCT_1:def_3; reconsider u1 = u1 as Variable by A42; consider a2 being Ordinal of W such that A44: a2 = g . (f . u1) and A45: f . u1 in L . a2 and for b being Ordinal of W st f . u1 in L . b holds a2 c= b by A15; a2 in g .: (rng f) by A15, A41, A43, A44, FUNCT_1:def_6; then a2 in b2 by ORDINAL2:19; then L . a2 c= L . a1 by A2, A37, A40, ORDINAL1:10; hence u in L . a1 by A43, A45; ::_thesis: verum end; set x = x. (k + 10); k + 0 = k ; then not k + 10 < k by XREAL_1:6; then not x. (k + 10) in variables_in H by A9; then A46: not x. (k + 10) in (variables_in H) \ {(x. 0)} by XBOOLE_0:def_5; set q = Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))); A47: 10 <= 10 + k by NAT_1:11; ( b0 c= b0 \/ b1 & b0 \/ b1 c= (b0 \/ b1) \/ b2 ) by XBOOLE_1:7; then b0 c= (b0 \/ b1) \/ b2 by XBOOLE_1:1; then A48: L . b0 c= L . a1 by A2, A37, ORDINAL1:12; then reconsider mu = u as Element of L . a1 by A29; dom f = VAR by FUNCT_2:def_1; then reconsider v = f as Function of VAR,(L . a1) by A39, FUNCT_2:def_1, RELSET_1:4; set w = (v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu); A49: ( x. (k + 10) <> x. (k + 5) implies not x. (k + 10) in {(x. (k + 5))} ) by TARSKI:def_1; ( variables_in (H / ((x. 0),(x. (k + 5)))) c= ((variables_in H) \ {(x. 0)}) \/ {(x. (k + 5))} & k + 5 <> k + 10 ) by ZF_LANG1:187; then not x. (k + 10) in variables_in (H / ((x. 0),(x. (k + 5)))) by A46, A49, XBOOLE_0:def_3, ZF_LANG1:76; then A50: ( variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) c= ((variables_in (H / ((x. 0),(x. (k + 5))))) \ {(x. 4)}) \/ {(x. 0)} & not x. (k + 10) in (variables_in (H / ((x. 0),(x. (k + 5))))) \ {(x. 4)} ) by XBOOLE_0:def_5, ZF_LANG1:187; A51: 10 > 0 ; then A52: x. (k + 10) <> x. 0 by A47, ZF_LANG1:76; then not x. (k + 10) in {(x. 0)} by TARSKI:def_1; then A53: not x. (k + 10) in variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A50, XBOOLE_0:def_3; A54: 10 > 3 ; then A55: ( x. 0 <> x. 3 & x. (k + 10) <> x. 3 ) by A47, ZF_LANG1:76; b0 \/ b1 in a1 by A37, ORDINAL1:12, XBOOLE_1:7; then L . (b0 \/ b1) c= L . a1 by A2; then A56: (def_func' (H,f)) .: u c= L . a1 by A34, XBOOLE_1:1; A57: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) proof now__::_thesis:_(def_func'_(H,f))_.:_u_=_Section_((Ex_((x._3),(((x._3)_'in'_(x._(k_+_10)))_'&'_((H_/_((x._0),(x._(k_+_5))))_/_((x._4),(x._0)))))),((v_/_((x._0),(v_._(x._4))))_/_((x._(k_+_10)),mu))) percases ( x. 4 in Free H or not x. 4 in Free H ) ; supposeA58: x. 4 in Free H ; ::_thesis: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) 4 <> k + 5 by NAT_1:11; then A59: x. (k + 5) <> x. 4 by ZF_LANG1:76; A60: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76; ( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76; then A61: x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))) by A58, A60, A59, Lm4; A62: (def_func' (H,f)) .: u c= Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) proof let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in (def_func' (H,f)) .: u or u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) ) assume A63: u1 in (def_func' (H,f)) .: u ; ::_thesis: u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) then consider u2 being set such that A64: u2 in dom (def_func' (H,f)) and A65: u2 in u and A66: u1 = (def_func' (H,f)) . u2 by FUNCT_1:def_6; reconsider m1 = u1 as Element of L . a1 by A56, A63; reconsider u2 = u2 as Element of Union L by A64; L . a1 is epsilon-transitive by A4; then u c= L . a1 by A29, A48, ORDINAL1:def_2; then reconsider m2 = u2 as Element of L . a1 by A65; A67: (f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2)) = (Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) by A66, ZF_LANG1:def_1, ZF_REFLE:16; ( Union L,(f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2)) |= H / ((x. 0),(x. (k + 5))) & ((f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2))) . (x. 4) = (def_func' (H,f)) . u2 ) by A11, A22, FUNCT_7:128, ZFMODEL2:10; then Union L,((f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2))) / ((x. 0),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A32, ZFMODEL2:13; then A68: Union L,((f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2))) / ((x. 4),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by FUNCT_7:33, ZF_LANG1:76; not x. 4 in variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by ZF_LANG1:76, ZF_LANG1:184; then Union L,(f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A68, ZFMODEL2:5; then L . a1,(v / ((x. 3),m2)) / ((x. 0),m1) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A36, A37, A38, A67; then A69: L . a1,((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (k + 10)),mu) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A53, ZFMODEL2:5; A70: ( ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) & ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; ( ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) = m2 & ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) ) by A54, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; then A71: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (x. 3) 'in' (x. (k + 10)) by A65, A70, ZF_MODEL:13; ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) = (v / ((x. (k + 10)),mu)) / ((x. 0),m1) by ZFMODEL2:8; then L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A52, A55, A69, ZFMODEL2:6; then L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A71, ZF_MODEL:15; then L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) by ZF_LANG1:73; then u1 in { m where m is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) } ; hence u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A61, Def1; ::_thesis: verum end; Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) c= (def_func' (H,f)) .: u proof let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) or u1 in (def_func' (H,f)) .: u ) A72: L . a1 c= Union L by ZF_REFLE:16; assume u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) ; ::_thesis: u1 in (def_func' (H,f)) .: u then u1 in { m where m is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) } by A61, Def1; then consider m1 being Element of L . a1 such that A73: u1 = m1 and A74: L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) ; consider m2 being Element of L . a1 such that A75: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A74, ZF_LANG1:73; ( m1 in L . a1 & m2 in L . a1 ) ; then reconsider u9 = m1, u2 = m2 as Element of Union L by A72; A76: ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) = (v / ((x. (k + 10)),mu)) / ((x. 0),m1) by ZFMODEL2:8; L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A75, ZF_MODEL:15; then L . a1,((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (k + 10)),mu) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A52, A55, A76, ZFMODEL2:6; then A77: L . a1,(v / ((x. 3),m2)) / ((x. 0),m1) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A53, ZFMODEL2:5; A78: ( ((f / ((x. 3),u2)) / ((x. 0),u9)) / ((x. 4),u9) = ((f / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) & ((f / ((x. 3),u2)) / ((x. 0),u9)) . (x. 0) = u9 ) by FUNCT_7:33, FUNCT_7:128, ZF_LANG1:76; (f / ((x. 3),u2)) / ((x. 0),u9) = (Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) by ZF_LANG1:def_1, ZF_REFLE:16; then Union L,(f / ((x. 3),u2)) / ((x. 0),u9) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A36, A37, A38, A77; then Union L,((f / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) |= H / ((x. 0),(x. (k + 5))) by A32, A78, ZFMODEL2:12; then Union L,(f / ((x. 3),u2)) / ((x. 4),u9) |= H / ((x. 0),(x. (k + 5))) by A32, ZFMODEL2:5; then A79: (def_func' (H,f)) . u2 = u9 by A11, A22, ZFMODEL2:10; A80: ( ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) & ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; A81: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (x. 3) 'in' (x. (k + 10)) by A75, ZF_MODEL:15; A82: dom (def_func' (H,f)) = Union L by FUNCT_2:def_1; ( ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) = m2 & ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) ) by A54, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76; then m2 in u by A81, A80, ZF_MODEL:13; hence u1 in (def_func' (H,f)) .: u by A73, A79, A82, FUNCT_1:def_6; ::_thesis: verum end; hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A62, XBOOLE_0:def_10; ::_thesis: verum end; supposeA83: not x. 4 in Free H ; ::_thesis: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) 4 <> k + 5 by NAT_1:11; then A84: x. (k + 5) <> x. 4 by ZF_LANG1:76; A85: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76; ( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76; then not x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))) by A83, A85, A84, Lm4; then Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) = {} by Def1; hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A8, A83, Lm3; ::_thesis: verum end; end; end; hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) ; ::_thesis: verum end; L . a1 in Union L by A4; hence (def_func' (H,f)) .: u in Union L by A5, A57, Def2; ::_thesis: verum end; Union L is epsilon-transitive proof let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L ) assume X in Union L ; ::_thesis: X c= Union L then consider u being set such that A86: u in dom L and A87: X in L . u by Lm1; reconsider u = u as Ordinal by A86; u in On W by A86, ZF_REFLE:def_2; then reconsider u = u as Ordinal of W by ZF_REFLE:7; L . u is epsilon-transitive by A4; then A88: X c= L . u by A87, ORDINAL1:def_2; let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L ) A89: L . u c= Union L by ZF_REFLE:16; assume u1 in X ; ::_thesis: u1 in Union L then u1 in L . u by A88; hence u1 in Union L by A89; ::_thesis: verum end; hence for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for H by A6, ZFMODEL1:15; ::_thesis: verum end; Lm5: for H being ZF-formula for M being non empty set for m being Element of M for v being Function of VAR,M for i being Element of NAT st x. i in Free H holds {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) proof let H be ZF-formula; ::_thesis: for M being non empty set for m being Element of M for v being Function of VAR,M for i being Element of NAT st x. i in Free H holds {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) let M be non empty set ; ::_thesis: for m being Element of M for v being Function of VAR,M for i being Element of NAT st x. i in Free H holds {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) let m be Element of M; ::_thesis: for v being Function of VAR,M for i being Element of NAT st x. i in Free H holds {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) let v be Function of VAR,M; ::_thesis: for i being Element of NAT st x. i in Free H holds {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) let i be Element of NAT ; ::_thesis: ( x. i in Free H implies {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) ) set e = (v / ((x. i),m)) * decode; set f = v * decode; set b = (v * decode) | ((code (Free H)) \ {i}); A1: i in {i} by TARSKI:def_1; A2: dom (((v / ((x. i),m)) * decode) | {i}) = (dom ((v / ((x. i),m)) * decode)) /\ {i} by RELAT_1:61 .= omega /\ {i} by ZF_FUND1:31 .= {i} by ZFMISC_1:46 ; then A3: ((v / ((x. i),m)) * decode) | {i} = {[i,((((v / ((x. i),m)) * decode) | {i}) . i)]} by GRFUNC_1:7 .= {[i,(((v / ((x. i),m)) * decode) . i)]} by A1, A2, FUNCT_1:47 .= {[i,(((v / ((x. i),m)) * decode) . (x". (x. i)))]} by ZF_FUND1:def_3 .= {[i,((v / ((x. i),m)) . (x. i))]} by ZF_FUND1:32 .= {[i,m]} by FUNCT_7:128 ; A4: dom ((v * decode) | ((code (Free H)) \ {i})) = (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61 .= omega /\ ((code (Free H)) \ {i}) by ZF_FUND1:31 .= (dom ((v / ((x. i),m)) * decode)) /\ ((code (Free H)) \ {i}) by ZF_FUND1:31 .= dom (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) by RELAT_1:61 ; now__::_thesis:_for_u_being_set_st_u_in_dom_((v_*_decode)_|_((code_(Free_H))_\_{i}))_holds_ ((v_*_decode)_|_((code_(Free_H))_\_{i}))_._u_=_(((v_/_((x._i),m))_*_decode)_|_((code_(Free_H))_\_{i}))_._u let u be set ; ::_thesis: ( u in dom ((v * decode) | ((code (Free H)) \ {i})) implies ((v * decode) | ((code (Free H)) \ {i})) . u = (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u ) assume A5: u in dom ((v * decode) | ((code (Free H)) \ {i})) ; ::_thesis: ((v * decode) | ((code (Free H)) \ {i})) . u = (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u then u in (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61; then A6: u in (code (Free H)) \ {i} by XBOOLE_0:def_4; then u in code (Free H) by XBOOLE_0:def_5; then consider x being Variable such that x in Free H and A7: u = x". x by ZF_FUND1:33; not u in {i} by A6, XBOOLE_0:def_5; then i <> x". x by A7, TARSKI:def_1; then A8: x <> x. i by ZF_FUND1:def_3; thus ((v * decode) | ((code (Free H)) \ {i})) . u = (v * decode) . u by A5, FUNCT_1:47 .= v . x by A7, ZF_FUND1:32 .= (v / ((x. i),m)) . x by A8, FUNCT_7:32 .= ((v / ((x. i),m)) * decode) . u by A7, ZF_FUND1:32 .= (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u by A4, A5, FUNCT_1:47 ; ::_thesis: verum end; then A9: (v * decode) | ((code (Free H)) \ {i}) = ((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i}) by A4, FUNCT_1:2; assume x. i in Free H ; ::_thesis: {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) then x". (x. i) in code (Free H) by ZF_FUND1:33; then i in code (Free H) by ZF_FUND1:def_3; then {i} c= code (Free H) by ZFMISC_1:31; then ((v / ((x. i),m)) * decode) | (code (Free H)) = ((v / ((x. i),m)) * decode) | ({i} \/ ((code (Free H)) \ {i})) by XBOOLE_1:45 .= {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) by A3, A9, RELAT_1:78 ; hence {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) ; ::_thesis: verum end; theorem Th4: :: ZF_FUND2:4 for H being ZF-formula for M being non empty set for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } proof let H be ZF-formula; ::_thesis: for M being non empty set for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } let M be non empty set ; ::_thesis: for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } let v be Function of VAR,M; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } set S = Section (H,v); set D = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; now__::_thesis:_Section_(H,v)_=__{__m_where_m_is_Element_of_M_:_{[{},m]}_\/_((v_*_decode)_|_((code_(Free_H))_\_{{}}))_in_Diagram_(H,M)__}_ percases ( x. 0 in Free H or not x. 0 in Free H ) ; supposeA1: x. 0 in Free H ; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } then A2: Section (H,v) = { m where m is Element of M : M,v / ((x. 0),m) |= H } by Def1; A3: { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } c= Section (H,v) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } or u in Section (H,v) ) assume u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; ::_thesis: u in Section (H,v) then consider m being Element of M such that A4: m = u and A5: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) ; ((v / ((x. 0),m)) * decode) | (code (Free H)) in Diagram (H,M) by A1, A5, Lm5; then ex v1 being Function of VAR,M st ( ((v / ((x. 0),m)) * decode) | (code (Free H)) = (v1 * decode) | (code (Free H)) & v1 in St (H,M) ) by ZF_FUND1:def_5; then v / ((x. 0),m) in St (H,M) by ZF_FUND1:36; then M,v / ((x. 0),m) |= H by ZF_MODEL:def_4; hence u in Section (H,v) by A2, A4; ::_thesis: verum end; Section (H,v) c= { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Section (H,v) or u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ) assume u in Section (H,v) ; ::_thesis: u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } then consider m being Element of M such that A6: m = u and A7: M,v / ((x. 0),m) |= H by A2; v / ((x. 0),m) in St (H,M) by A7, ZF_MODEL:def_4; then ((v / ((x. 0),m)) * decode) | (code (Free H)) in Diagram (H,M) by ZF_FUND1:def_5; then {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) by A1, Lm5; hence u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A6; ::_thesis: verum end; hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A3, XBOOLE_0:def_10; ::_thesis: verum end; supposeA8: not x. 0 in Free H ; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } now__::_thesis:_not__{__m_where_m_is_Element_of_M_:_{[{},m]}_\/_((v_*_decode)_|_((code_(Free_H))_\_{{}}))_in_Diagram_(H,M)__}__<>_{} set u = the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; assume { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } <> {} ; ::_thesis: contradiction then the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; then consider m being Element of M such that m = the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } and A9: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) ; consider v2 being Function of VAR,M such that A10: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) = (v2 * decode) | (code (Free H)) and v2 in St (H,M) by A9, ZF_FUND1:def_5; reconsider w = {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) as Function by A10; [{},m] in {[{},m]} by TARSKI:def_1; then [{},m] in w by XBOOLE_0:def_3; then {} in dom w by FUNCT_1:1; then {} in (dom (v2 * decode)) /\ (code (Free H)) by A10, RELAT_1:61; then {} in code (Free H) by XBOOLE_0:def_4; then ex y being Variable st ( y in Free H & {} = x". y ) by ZF_FUND1:33; hence contradiction by A8, ZF_FUND1:def_3; ::_thesis: verum end; hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A8, Def1; ::_thesis: verum end; end; end; hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; ::_thesis: verum end; theorem Th5: :: ZF_FUND2:5 for W being Universe for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds Y is predicatively_closed proof let W be Universe; ::_thesis: for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds Y is predicatively_closed let Y be Subclass of W; ::_thesis: ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed ) assume that A1: Y is closed_wrt_A1-A7 and A2: Y is epsilon-transitive ; ::_thesis: Y is predicatively_closed let H be ZF-formula; :: according to ZF_FUND2:def_2 ::_thesis: for E being non empty set for f being Function of VAR,E st E in Y holds Section (H,f) in Y let E be non empty set ; ::_thesis: for f being Function of VAR,E st E in Y holds Section (H,f) in Y let f be Function of VAR,E; ::_thesis: ( E in Y implies Section (H,f) in Y ) assume A3: E in Y ; ::_thesis: Section (H,f) in Y now__::_thesis:_Section_(H,f)_in_Y percases ( not x. 0 in Free H or x. 0 in Free H ) ; suppose not x. 0 in Free H ; ::_thesis: Section (H,f) in Y then Section (H,f) = {} by Def1; hence Section (H,f) in Y by A1, ZF_FUND1:3; ::_thesis: verum end; supposeA4: x. 0 in Free H ; ::_thesis: Section (H,f) in Y reconsider a = E as Element of W by A3; reconsider n = {} as Element of omega by ORDINAL1:def_11; set fs = (code (Free H)) \ {n}; A5: Diagram (H,E) in Y by A1, A3, ZF_FUND1:22; then reconsider b = Diagram (H,E) as Element of W ; A6: b c= Funcs ((((code (Free H)) \ {n}) \/ {n}),a) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in b or u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) ) assume u in b ; ::_thesis: u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) then ex f1 being Function of VAR,E st ( u = (f1 * decode) | (code (Free H)) & f1 in St (H,E) ) by ZF_FUND1:def_5; then A7: u in Funcs ((code (Free H)),a) by ZF_FUND1:31; x". (x. 0) in code (Free H) by A4, ZF_FUND1:33; then n in code (Free H) by ZF_FUND1:def_3; then {n} c= code (Free H) by ZFMISC_1:31; hence u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) by A7, XBOOLE_1:45; ::_thesis: verum end; n in {n} by TARSKI:def_1; then A8: not n in (code (Free H)) \ {n} by XBOOLE_0:def_5; A9: (f * decode) | ((code (Free H)) \ {n}) in Funcs (((code (Free H)) \ {n}),a) by ZF_FUND1:31; Funcs (((code (Free H)) \ {n}),a) in Y by A1, A3, ZF_FUND1:9; then reconsider y = (f * decode) | ((code (Free H)) \ {n}) as Element of W by A9, ZF_FUND1:1; set B = { e where e is Element of E : {[n,e]} \/ y in b } ; set A = { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ; A10: { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } = { e where e is Element of E : {[n,e]} \/ y in b } proof thus { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } c= { e where e is Element of E : {[n,e]} \/ y in b } :: according to XBOOLE_0:def_10 ::_thesis: { e where e is Element of E : {[n,e]} \/ y in b } c= { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } or u in { e where e is Element of E : {[n,e]} \/ y in b } ) assume u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ; ::_thesis: u in { e where e is Element of E : {[n,e]} \/ y in b } then ex w being Element of W st ( u = w & w in a & {[n,w]} \/ y in b ) ; hence u in { e where e is Element of E : {[n,e]} \/ y in b } ; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { e where e is Element of E : {[n,e]} \/ y in b } or u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ) assume u in { e where e is Element of E : {[n,e]} \/ y in b } ; ::_thesis: u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } then consider e being Element of E such that A11: u = e and A12: {[n,e]} \/ y in b ; reconsider e = e as Element of W by A3, ZF_FUND1:1; e in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A12; hence u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A11; ::_thesis: verum end; a c= Y by A2, A3, ORDINAL1:def_2; then { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } in Y by A1, A3, A5, A9, A8, A6, ZF_FUND1:16; hence Section (H,f) in Y by A10, Th4; ::_thesis: verum end; end; end; hence Section (H,f) in Y ; ::_thesis: verum end; theorem :: ZF_FUND2:6 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds Union L is being_a_model_of_ZF 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds Union L is being_a_model_of_ZF 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) ) & ( for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 implies Union L is being_a_model_of_ZF ) 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) and A4: for a being Ordinal of W holds ( L . a in Union L & L . a is epsilon-transitive ) and A5: Union L is closed_wrt_A1-A7 ; ::_thesis: Union L is being_a_model_of_ZF A6: Union L is epsilon-transitive proof let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L ) assume X in Union L ; ::_thesis: X c= Union L then consider u being set such that A7: u in dom L and A8: X in L . u by Lm1; reconsider u = u as Ordinal by A7; u in On W by A7, ZF_REFLE:def_2; then reconsider u = u as Ordinal of W by ZF_REFLE:7; L . u is epsilon-transitive by A4; then A9: X c= L . u by A8, ORDINAL1:def_2; let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L ) A10: L . u c= Union L by ZF_REFLE:16; assume u1 in X ; ::_thesis: u1 in Union L then u1 in L . u by A9; hence u1 in Union L by A10; ::_thesis: verum end; then Union L is predicatively_closed by A5, Th5; then A11: ( Union L |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds Union L |= the_axiom_of_substitution_for H ) ) by A1, A2, A3, A4, Th2, Th3; for u being set st u in Union L holds union u in Union L by A5, ZF_FUND1:2; then A12: Union L |= the_axiom_of_unions by A6, ZFMODEL1:5; for u1, u2 being set st u1 in Union L & u2 in Union L holds {u1,u2} in Union L by A5, ZF_FUND1:6; then A13: Union L |= the_axiom_of_pairs by A6, ZFMODEL1:3; ex u being set st ( u in Union L & u <> {} & ( for u1 being set st u1 in u holds ex u2 being set st ( u1 c< u2 & u2 in u ) ) ) proof A14: card omega in card W by A1, CLASSES2:1; deffunc H1( set , set ) -> set = inf { w where w is Element of W : L . $2 in L . w } ; consider ksi being Function such that A15: ( dom ksi = NAT & ksi . 0 = 0-element_of W & ( for i being Nat holds ksi . (i + 1) = H1(i,ksi . i) ) ) from NAT_1:sch_11(); card (rng ksi) c= card NAT by A15, CARD_1:12; then A16: card (rng ksi) in card W by A14, ORDINAL1:12; set lambda = sup (rng ksi); A17: for i being Element of NAT holds ( ksi . i in On W & ksi . i is Ordinal of W ) proof defpred S1[ Element of NAT ] means ( ksi . $1 in On W & ksi . $1 is Ordinal of W ); A18: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_ S1[i_+_1] let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume S1[i] ; ::_thesis: S1[i + 1] then reconsider a = ksi . i as Ordinal of W ; A19: ksi . (i + 1) = inf { w where w is Element of W : L . a in L . w } by A15; consider u being set such that A20: u in dom L and A21: L . a in L . u by A4, Lm1; dom L = On W by ZF_REFLE:def_2; then reconsider b = u as Ordinal of W by A20, ZF_REFLE:7; b in { w where w is Element of W : L . a in L . w } by A21; then inf { w where w is Element of W : L . a in L . w } c= b by ORDINAL2:14; then ksi . (i + 1) in W by A19, CLASSES1:def_1; hence S1[i + 1] by A19, ORDINAL1:def_9; ::_thesis: verum end; A22: S1[ 0 ] by A15, ZF_REFLE:7; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A22, A18); ::_thesis: verum end; rng ksi c= W proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng ksi or a in W ) assume a in rng ksi ; ::_thesis: a in W then consider i being set such that A23: i in dom ksi and A24: a = ksi . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A15, A23; ksi . i in On W by A17; hence a in W by A24, ORDINAL1:def_9; ::_thesis: verum end; then rng ksi in W by A16, CLASSES1:1; then reconsider l = sup (rng ksi) as Ordinal of W by ZF_REFLE:19; A25: for i being Element of NAT holds L . (ksi . i) in L . (ksi . (i + 1)) proof let i be Element of NAT ; ::_thesis: L . (ksi . i) in L . (ksi . (i + 1)) reconsider a = ksi . i as Ordinal of W by A17; consider b being set such that A26: b in dom L and A27: L . a in L . b by A4, Lm1; b in On W by A26, ZF_REFLE:def_2; then reconsider b = b as Ordinal of W by ZF_REFLE:7; A28: b in { w where w is Element of W : L . a in L . w } by A27; ksi . (i + 1) = inf { w where w is Element of W : L . (ksi . i) in L . w } by A15; then ksi . (i + 1) in { w where w is Element of W : L . (ksi . i) in L . w } by A28, ORDINAL2:17; then ex w being Element of W st ( w = ksi . (i + 1) & L . a in L . w ) ; hence L . (ksi . i) in L . (ksi . (i + 1)) ; ::_thesis: verum end; A29: for i being Element of NAT holds ksi . i in ksi . (i + 1) proof let i be Element of NAT ; ::_thesis: ksi . i in ksi . (i + 1) reconsider b = ksi . (i + 1) as Ordinal of W by A17; reconsider a = ksi . i as Ordinal of W by A17; assume not ksi . i in ksi . (i + 1) ; ::_thesis: contradiction then ( b = a or b in a ) by ORDINAL1:14; then L . b c= L . a by A2; hence contradiction by A25, ORDINAL1:5; ::_thesis: verum end; A30: l c= union l proof let u1 be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not u1 in l or u1 in union l ) assume u1 in l ; ::_thesis: u1 in union l then consider u2 being Ordinal such that A31: u2 in rng ksi and A32: u1 c= u2 by ORDINAL2:21; consider i being set such that A33: i in dom ksi and A34: u2 = ksi . i by A31, FUNCT_1:def_3; reconsider i = i as Element of NAT by A15, A33; reconsider u3 = ksi . (i + 1) as Ordinal of W by A17; u3 in rng ksi by A15, FUNCT_1:def_3; then A35: u3 in l by ORDINAL2:19; u1 in u3 by A29, A32, A34, ORDINAL1:12; hence u1 in union l by A35, TARSKI:def_4; ::_thesis: verum end; union l c= l by ORDINAL2:5; then l = union l by A30, XBOOLE_0:def_10; then A36: l is limit_ordinal by ORDINAL1:def_6; A37: union { (L . (ksi . n)) where n is Element of NAT : verum } = L . l proof set A = { (L . (ksi . n)) where n is Element of NAT : verum } ; thus union { (L . (ksi . n)) where n is Element of NAT : verum } c= L . l :: according to XBOOLE_0:def_10 ::_thesis: L . l c= union { (L . (ksi . n)) where n is Element of NAT : verum } proof let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } or u1 in L . l ) assume u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } ; ::_thesis: u1 in L . l then consider X being set such that A38: u1 in X and A39: X in { (L . (ksi . n)) where n is Element of NAT : verum } by TARSKI:def_4; consider n being Element of NAT such that A40: X = L . (ksi . n) by A39; reconsider a = ksi . n as Ordinal of W by A17; a in rng ksi by A15, FUNCT_1:def_3; then L . a c= L . l by A2, ORDINAL2:19; hence u1 in L . l by A38, A40; ::_thesis: verum end; 0-element_of W in rng ksi by A15, FUNCT_1:def_3; then l <> {} by ORDINAL2:19; then A41: L . l = Union (L | l) by A3, A36; let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in L . l or u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } ) assume u1 in L . l ; ::_thesis: u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } then consider u2 being set such that A42: u2 in dom (L | l) and A43: u1 in (L | l) . u2 by A41, Lm1; A44: u1 in L . u2 by A42, A43, FUNCT_1:47; A45: u2 in (dom L) /\ l by A42, RELAT_1:61; then A46: u2 in l by XBOOLE_0:def_4; u2 in dom L by A45, XBOOLE_0:def_4; then u2 in On W by ZF_REFLE:def_2; then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7; consider b being Ordinal such that A47: b in rng ksi and A48: u2 c= b by A46, ORDINAL2:21; consider i being set such that A49: i in dom ksi and A50: b = ksi . i by A47, FUNCT_1:def_3; reconsider i = i as Element of NAT by A15, A49; b = ksi . i by A50; then reconsider b = b as Ordinal of W by A17; ( u2 c< b iff ( u2 c= b & u2 <> b ) ) by XBOOLE_0:def_8; then A51: L . u2 c= L . b by A2, A48, ORDINAL1:11; L . (ksi . i) in { (L . (ksi . n)) where n is Element of NAT : verum } ; hence u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } by A44, A50, A51, TARSKI:def_4; ::_thesis: verum end; take u = L . (sup (rng ksi)); ::_thesis: ( u in Union L & u <> {} & ( for u1 being set st u1 in u holds ex u2 being set st ( u1 c< u2 & u2 in u ) ) ) L . l in Union L by A4; hence ( u in Union L & u <> {} ) ; ::_thesis: for u1 being set st u1 in u holds ex u2 being set st ( u1 c< u2 & u2 in u ) let u1 be set ; ::_thesis: ( u1 in u implies ex u2 being set st ( u1 c< u2 & u2 in u ) ) assume u1 in u ; ::_thesis: ex u2 being set st ( u1 c< u2 & u2 in u ) then consider u2 being set such that A52: ( u1 in u2 & u2 in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A37, TARSKI:def_4; take u2 ; ::_thesis: ( u1 c< u2 & u2 in u ) consider i being Element of NAT such that A53: u2 = L . (ksi . i) by A52; A54: u1 <> u2 by A52; reconsider a = ksi . i as Ordinal of W by A17; L . a is epsilon-transitive by A4; then u1 c= u2 by A52, A53, ORDINAL1:def_2; hence u1 c< u2 by A54, XBOOLE_0:def_8; ::_thesis: u2 in u A55: L . (ksi . (i + 1)) in { (L . (ksi . n)) where n is Element of NAT : verum } ; L . (ksi . i) in L . (ksi . (i + 1)) by A25; hence u2 in u by A37, A53, A55, TARSKI:def_4; ::_thesis: verum end; then Union L |= the_axiom_of_infinity by A6, ZFMODEL1:7; hence Union L is being_a_model_of_ZF by A6, A13, A12, A11, ZF_MODEL:def_12; ::_thesis: verum end;