:: CARD_5 semantic presentation begin Lm1: 1 = card 1 by CARD_1:def_2; Lm2: 2 = card 2 by CARD_1:def_2; begin theorem Th1: :: CARD_5:1 for X being set holds nextcard (card X) = nextcard X proof let X be set ; ::_thesis: nextcard (card X) = nextcard X ( card (card X) in nextcard X & ( for M being Cardinal st card (card X) in M holds nextcard X c= M ) ) by CARD_1:def_3; hence nextcard (card X) = nextcard X by CARD_1:def_3; ::_thesis: verum end; theorem Th2: :: CARD_5:2 for y being set for f being Function holds ( y in Union f iff ex x being set st ( x in dom f & y in f . x ) ) proof let y be set ; ::_thesis: for f being Function holds ( y in Union f iff ex x being set st ( x in dom f & y in f . x ) ) let f be Function; ::_thesis: ( y in Union f iff ex x being set st ( x in dom f & y in f . x ) ) thus ( y in Union f implies ex x being set st ( x in dom f & y in f . x ) ) ::_thesis: ( ex x being set st ( x in dom f & y in f . x ) implies y in Union f ) proof assume y in Union f ; ::_thesis: ex x being set st ( x in dom f & y in f . x ) then consider X being set such that A1: y in X and A2: X in rng f by TARSKI:def_4; consider x being set such that A3: ( x in dom f & X = f . x ) by A2, FUNCT_1:def_3; take x ; ::_thesis: ( x in dom f & y in f . x ) thus ( x in dom f & y in f . x ) by A1, A3; ::_thesis: verum end; given x being set such that A4: x in dom f and A5: y in f . x ; ::_thesis: y in Union f f . x in rng f by A4, FUNCT_1:def_3; hence y in Union f by A5, TARSKI:def_4; ::_thesis: verum end; theorem Th3: :: CARD_5:3 for A being Ordinal holds alef A is infinite proof let A be Ordinal; ::_thesis: alef A is infinite {} c= A by XBOOLE_1:2; then omega c= alef A by CARD_1:23, CARD_1:46; hence alef A is infinite ; ::_thesis: verum end; theorem Th4: :: CARD_5:4 for M being Cardinal st M is infinite holds ex A being Ordinal st M = alef A proof let M be Cardinal; ::_thesis: ( M is infinite implies ex A being Ordinal st M = alef A ) defpred S1[ set ] means ( $1 is infinite implies ex A being Ordinal st $1 = alef A ); A1: for K being Cardinal st S1[K] holds S1[ nextcard K] proof let K be Cardinal; ::_thesis: ( S1[K] implies S1[ nextcard K] ) assume that A2: S1[K] and A3: not nextcard K is finite ; ::_thesis: ex A being Ordinal st nextcard K = alef A now__::_thesis:_not_K_is_finite assume K is finite ; ::_thesis: contradiction then reconsider K9 = K as finite set ; card K = K by CARD_1:def_2; then nextcard K = card ((card K9) + 1) by NAT_1:42; hence contradiction by A3; ::_thesis: verum end; then consider A being Ordinal such that A4: K = alef A by A2; take succ A ; ::_thesis: nextcard K = alef (succ A) thus nextcard K = alef (succ A) by A4, CARD_1:19; ::_thesis: verum end; A5: for K being Cardinal st K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds S1[N] ) holds S1[K] proof let K be Cardinal; ::_thesis: ( K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds S1[N] ) implies S1[K] ) deffunc H1( Ordinal) -> set = alef $1; defpred S2[ set , set ] means ex A being Ordinal st ( $1 = alef A & $2 = A ); assume that K <> {} and A6: K is limit_cardinal and A7: for N being Cardinal st N in K holds S1[N] and A8: not K is finite ; ::_thesis: ex A being Ordinal st K = alef A defpred S3[ set ] means ex N being Cardinal st ( N = $1 & not N is finite ); consider X being set such that A9: for x being set holds ( x in X iff ( x in K & S3[x] ) ) from XBOOLE_0:sch_1(); A10: for x being set st x in X holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in X implies ex y being set st S2[x,y] ) assume A11: x in X ; ::_thesis: ex y being set st S2[x,y] then consider N being Cardinal such that A12: N = x and A13: not N is finite by A9; N in K by A9, A11, A12; then ex A being Ordinal st x = alef A by A7, A12, A13; hence ex y being set st S2[x,y] ; ::_thesis: verum end; consider f being Function such that A14: ( dom f = X & ( for x being set st x in X holds S2[x,f . x] ) ) from CLASSES1:sch_1(A10); now__::_thesis:_for_x_being_set_st_x_in_rng_f_holds_ (_x_is_Ordinal_&_x_c=_rng_f_) let x be set ; ::_thesis: ( x in rng f implies ( x is Ordinal & x c= rng f ) ) assume x in rng f ; ::_thesis: ( x is Ordinal & x c= rng f ) then consider y being set such that A15: y in X and A16: x = f . y by A14, FUNCT_1:def_3; consider A being Ordinal such that A17: y = alef A and A18: x = A by A14, A15, A16; thus x is Ordinal by A18; ::_thesis: x c= rng f thus x c= rng f ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in rng f ) assume A19: z in x ; ::_thesis: z in rng f then reconsider z9 = z as Ordinal by A18; A20: alef z9 in alef A by A18, A19, CARD_1:21; alef A in K by A9, A15, A17; then A21: alef z9 in K by A20, ORDINAL1:10; not alef z9 is finite by Th3; then A22: alef z9 in X by A9, A21; then ex A being Ordinal st ( alef z9 = alef A & f . (alef z9) = A ) by A14; then z9 = f . (alef z9) by CARD_1:22; hence z in rng f by A14, A22, FUNCT_1:def_3; ::_thesis: verum end; end; then reconsider A = rng f as Ordinal by ORDINAL1:19; consider L being T-Sequence such that A23: ( dom L = A & ( for B being Ordinal st B in A holds L . B = H1(B) ) ) from ORDINAL2:sch_2(); now__::_thesis:_for_B_being_Ordinal_st_B_in_A_holds_ succ_B_in_A let B be Ordinal; ::_thesis: ( B in A implies succ B in A ) assume B in A ; ::_thesis: succ B in A then consider x being set such that A24: x in X and A25: B = f . x by A14, FUNCT_1:def_3; consider C being Ordinal such that A26: x = alef C and A27: B = C by A14, A24, A25; A28: alef (succ C) = nextcard (alef C) by CARD_1:19; alef C in K by A9, A24, A26; then A29: alef (succ C) c= K by A28, CARD_3:90; alef (succ C) <> K by A6, A28, CARD_1:def_4; then A30: alef (succ C) in K by A29, CARD_1:3; not alef (succ C) is finite by Th3; then A31: alef (succ C) in X by A9, A30; then consider D being Ordinal such that A32: alef (succ C) = alef D and A33: f . (alef (succ C)) = D by A14; succ C = D by A32, CARD_1:22; hence succ B in A by A14, A27, A31, A33, FUNCT_1:def_3; ::_thesis: verum end; then A is limit_ordinal by ORDINAL1:28; then A34: ( A = {} or alef A = card (sup L) ) by A23, CARD_1:20; take A ; ::_thesis: K = alef A sup L c= K proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup L or x in K ) assume A35: x in sup L ; ::_thesis: x in K then reconsider x9 = x as Ordinal ; consider C being Ordinal such that A36: C in rng L and A37: x9 c= C by A35, ORDINAL2:21; consider y being set such that A38: y in dom L and A39: C = L . y by A36, FUNCT_1:def_3; reconsider y = y as Ordinal by A38; A40: C = alef y by A23, A38, A39; consider z being set such that A41: z in dom f and A42: y = f . z by A23, A38, FUNCT_1:def_3; ex D being Ordinal st ( z = alef D & y = D ) by A14, A41, A42; then C in K by A9, A14, A40, A41; hence x in K by A37, ORDINAL1:12; ::_thesis: verum end; then card (sup L) c= card K by CARD_1:11; then A43: card (sup L) c= K by CARD_1:def_2; now__::_thesis:_(_(_A_=_{}_&_K_=_omega_)_or_(_A_<>_{}_&_not_K_<>_alef_A_)_) percases ( A = {} or A <> {} ) ; case A = {} ; ::_thesis: K = omega then not omega in X by A14, RELAT_1:42; then not omega in K by A9; then A44: K c= omega by CARD_1:4; omega c= K by A8, CARD_3:85; hence K = omega by A44, XBOOLE_0:def_10; ::_thesis: verum end; caseA45: A <> {} ; ::_thesis: not K <> alef A assume K <> alef A ; ::_thesis: contradiction then A46: card (sup L) in K by A34, A43, A45, CARD_1:3; not alef A is finite by Th3; then A47: card (sup L) in X by A9, A34, A45, A46; then consider B being Ordinal such that A48: card (sup L) = alef B and A49: f . (card (sup L)) = B by A14; A = B by A34, A45, A48, CARD_1:22; then A in A by A14, A47, A49, FUNCT_1:def_3; hence contradiction ; ::_thesis: verum end; end; end; hence K = alef A by CARD_1:46; ::_thesis: verum end; A50: S1[ {} ] ; for M being Cardinal holds S1[M] from CARD_1:sch_1(A50, A1, A5); hence ( M is infinite implies ex A being Ordinal st M = alef A ) ; ::_thesis: verum end; registration let phi be Ordinal-Sequence; cluster Union phi -> ordinal ; coherence Union phi is ordinal proof ex A being Ordinal st rng phi c= A by ORDINAL2:def_4; then On (rng phi) = rng phi by ORDINAL3:6; hence Union phi is ordinal by ORDINAL3:5; ::_thesis: verum end; end; theorem Th5: :: CARD_5:5 for A being Ordinal for X being set st X c= A holds ex phi being Ordinal-Sequence st ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) proof let A be Ordinal; ::_thesis: for X being set st X c= A holds ex phi being Ordinal-Sequence st ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) let X be set ; ::_thesis: ( X c= A implies ex phi being Ordinal-Sequence st ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) ) set R = RelIncl X; set B = order_type_of (RelIncl X); set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)); assume A1: X c= A ; ::_thesis: ex phi being Ordinal-Sequence st ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) then RelIncl X is well-ordering by WELLORD2:8; then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2; then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8; then A2: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9; then A3: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by WELLORD1:def_7; A4: field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1; then A5: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A2, WELLORD1:def_7; A6: field (RelIncl X) = X by WELLORD2:def_1; then A7: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A2, WELLORD1:def_7; reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as T-Sequence by A5, ORDINAL1:def_7; reconsider phi = phi as Ordinal-Sequence by A1, A7, ORDINAL2:def_4; take phi ; ::_thesis: ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) thus phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) ; ::_thesis: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) thus phi is increasing ::_thesis: ( dom phi = order_type_of (RelIncl X) & rng phi = X ) proof let a, b be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not a in b or not b in dom phi or phi . a in phi . b ) assume that A8: a in b and A9: b in dom phi ; ::_thesis: phi . a in phi . b A10: a in dom phi by A8, A9, ORDINAL1:10; reconsider a9 = phi . a, b9 = phi . b as Ordinal ; A11: b9 in X by A7, A9, FUNCT_1:def_3; a c= b by A8, ORDINAL1:def_2; then [a,b] in RelIncl (order_type_of (RelIncl X)) by A5, A9, A10, WELLORD2:def_1; then A12: [a9,b9] in RelIncl X by A2, WELLORD1:def_7; a9 in X by A7, A10, FUNCT_1:def_3; then A13: a9 c= b9 by A12, A11, WELLORD2:def_1; a <> b by A8; then a9 <> b9 by A3, A9, A10, FUNCT_1:def_4; then a9 c< b9 by A13, XBOOLE_0:def_8; hence phi . a in phi . b by ORDINAL1:11; ::_thesis: verum end; thus ( dom phi = order_type_of (RelIncl X) & rng phi = X ) by A2, A4, A6, WELLORD1:def_7; ::_thesis: verum end; theorem Th6: :: CARD_5:6 for A being Ordinal for X being set st X c= A holds sup X is_cofinal_with order_type_of (RelIncl X) proof let A be Ordinal; ::_thesis: for X being set st X c= A holds sup X is_cofinal_with order_type_of (RelIncl X) let X be set ; ::_thesis: ( X c= A implies sup X is_cofinal_with order_type_of (RelIncl X) ) assume A1: X c= A ; ::_thesis: sup X is_cofinal_with order_type_of (RelIncl X) then consider phi being Ordinal-Sequence such that phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and A2: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) by Th5; take phi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi ) On X = X by A1, ORDINAL3:6; hence ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi ) by A2, ORDINAL2:def_3; ::_thesis: verum end; theorem Th7: :: CARD_5:7 for A being Ordinal for X being set st X c= A holds card X = card (order_type_of (RelIncl X)) proof let A be Ordinal; ::_thesis: for X being set st X c= A holds card X = card (order_type_of (RelIncl X)) let X be set ; ::_thesis: ( X c= A implies card X = card (order_type_of (RelIncl X)) ) set R = RelIncl X; set B = order_type_of (RelIncl X); set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)); assume X c= A ; ::_thesis: card X = card (order_type_of (RelIncl X)) then RelIncl X is well-ordering by WELLORD2:8; then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2; then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8; then A1: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9; field (RelIncl X) = X by WELLORD2:def_1; then A2: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A1, WELLORD1:def_7; field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1; then A3: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A1, WELLORD1:def_7; canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by A1, WELLORD1:def_7; then order_type_of (RelIncl X),X are_equipotent by A3, A2, WELLORD2:def_4; hence card X = card (order_type_of (RelIncl X)) by CARD_1:5; ::_thesis: verum end; theorem Th8: :: CARD_5:8 for A being Ordinal ex B being Ordinal st ( B c= card A & A is_cofinal_with B ) proof let A be Ordinal; ::_thesis: ex B being Ordinal st ( B c= card A & A is_cofinal_with B ) set M = card A; card A,A are_equipotent by CARD_1:def_2; then consider f being Function such that A1: f is one-to-one and A2: dom f = card A and A3: rng f = A by WELLORD2:def_4; defpred S1[ set ] means not f . $1 in Union (f | $1); reconsider f = f as T-Sequence by A2, ORDINAL1:def_7; reconsider f = f as Ordinal-Sequence by A3, ORDINAL2:def_4; consider X being set such that A4: for x being set holds ( x in X iff ( x in card A & S1[x] ) ) from XBOOLE_0:sch_1(); set R = RelIncl X; set B = order_type_of (RelIncl X); take order_type_of (RelIncl X) ; ::_thesis: ( order_type_of (RelIncl X) c= card A & A is_cofinal_with order_type_of (RelIncl X) ) A5: X c= card A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in card A ) thus ( not x in X or x in card A ) by A4; ::_thesis: verum end; hence order_type_of (RelIncl X) c= card A by WELLORD2:14; ::_thesis: A is_cofinal_with order_type_of (RelIncl X) set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)); RelIncl X is well-ordering by A5, WELLORD2:8; then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2; then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8; then A6: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def_9; then A7: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by WELLORD1:def_7; field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def_1; then A8: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A6, WELLORD1:def_7; field (RelIncl X) = X by WELLORD2:def_1; then A9: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A6, WELLORD1:def_7; reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as T-Sequence by A8, ORDINAL1:def_7; reconsider phi = phi as Ordinal-Sequence by A5, A9, ORDINAL2:def_4; A10: dom (f * phi) = order_type_of (RelIncl X) by A2, A5, A8, A9, RELAT_1:27; then reconsider xi = f * phi as T-Sequence by ORDINAL1:def_7; rng (f * phi) c= A by A3, RELAT_1:26; then reconsider xi = xi as Ordinal-Sequence by ORDINAL2:def_4; take xi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom xi = order_type_of (RelIncl X) & rng xi c= A & xi is increasing & A = sup xi ) thus ( dom xi = order_type_of (RelIncl X) & rng xi c= A ) by A2, A3, A5, A8, A9, RELAT_1:26, RELAT_1:27; ::_thesis: ( xi is increasing & A = sup xi ) thus xi is increasing ::_thesis: A = sup xi proof let a, b be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not a in b or not b in dom xi or xi . a in xi . b ) assume that A11: a in b and A12: b in dom xi ; ::_thesis: xi . a in xi . b A13: a in dom xi by A11, A12, ORDINAL1:10; then A14: phi . a in X by A8, A9, A10, FUNCT_1:def_3; a <> b by A11; then A15: phi . a <> phi . b by A8, A7, A10, A12, A13, FUNCT_1:def_4; reconsider a9 = phi . a, b9 = phi . b as Ordinal ; reconsider a99 = f . a9, b99 = f . b9 as Ordinal ; A16: phi . b in X by A8, A9, A10, A12, FUNCT_1:def_3; then not b99 in Union (f | b9) by A4; then A17: Union (f | b9) c= b99 by ORDINAL1:16; a c= b by A11, ORDINAL1:def_2; then [a,b] in RelIncl (order_type_of (RelIncl X)) by A10, A12, A13, WELLORD2:def_1; then [(phi . a),(phi . b)] in RelIncl X by A6, WELLORD1:def_7; then a9 c= b9 by A14, A16, WELLORD2:def_1; then a9 c< b9 by A15, XBOOLE_0:def_8; then a9 in b9 by ORDINAL1:11; then a99 c= Union (f | b9) by A2, A5, A14, FUNCT_1:50, ZFMISC_1:74; then A18: a99 c= b99 by A17, XBOOLE_1:1; a99 <> b99 by A1, A2, A5, A15, A14, A16, FUNCT_1:def_4; then A19: a99 c< b99 by A18, XBOOLE_0:def_8; ( a99 = xi . a & b99 = xi . b ) by A11, A12, FUNCT_1:12, ORDINAL1:10; hence xi . a in xi . b by A19, ORDINAL1:11; ::_thesis: verum end; thus A c= sup xi :: according to XBOOLE_0:def_10 ::_thesis: sup xi c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup xi ) assume x in A ; ::_thesis: x in sup xi then consider y being set such that A20: y in dom f and A21: x = f . y by A3, FUNCT_1:def_3; reconsider x9 = x, y = y as Ordinal by A20, A21; now__::_thesis:_x_in_sup_xi percases ( not f . y in Union (f | y) or f . y in Union (f | y) ) ; suppose not f . y in Union (f | y) ; ::_thesis: x in sup xi then y in X by A2, A4, A20; then consider z being set such that A22: ( z in order_type_of (RelIncl X) & y = phi . z ) by A8, A9, FUNCT_1:def_3; ( x9 = xi . z & xi . z in rng xi ) by A10, A21, A22, FUNCT_1:12, FUNCT_1:def_3; hence x in sup xi by ORDINAL2:19; ::_thesis: verum end; supposeA23: f . y in Union (f | y) ; ::_thesis: x in sup xi defpred S2[ Ordinal] means ( $1 in y & f . y in f . $1 ); consider z being set such that A24: z in dom (f | y) and A25: f . y in (f | y) . z by A23, Th2; reconsider z = z as Ordinal by A24; A26: (f | y) . z = f . z by A24, FUNCT_1:47; dom (f | y) = (dom f) /\ y by RELAT_1:61; then z in y by A24, XBOOLE_0:def_4; then A27: ex C being Ordinal st S2[C] by A25, A26; consider C being Ordinal such that A28: ( S2[C] & ( for B being Ordinal st S2[B] holds C c= B ) ) from ORDINAL1:sch_1(A27); now__::_thesis:_(_C_in_card_A_&_not_f_._C_in_Union_(f_|_C)_) thus C in card A by A2, A20, A28, ORDINAL1:10; ::_thesis: not f . C in Union (f | C) assume f . C in Union (f | C) ; ::_thesis: contradiction then consider a being set such that A29: a in dom (f | C) and A30: f . C in (f | C) . a by Th2; reconsider a = a as Ordinal by A29; reconsider fa = (f | C) . a, fy = f . y as Ordinal ; f . a = fa by A29, FUNCT_1:47; then A31: fy in f . a by A28, A30, ORDINAL1:10; dom (f | C) = (dom f) /\ C by RELAT_1:61; then A32: a in C by A29, XBOOLE_0:def_4; then a in y by A28, ORDINAL1:10; hence contradiction by A28, A32, A31, ORDINAL1:5; ::_thesis: verum end; then C in X by A4; then consider z being set such that A33: z in order_type_of (RelIncl X) and A34: C = phi . z by A8, A9, FUNCT_1:def_3; reconsider z = z as Ordinal by A33; reconsider xz = xi . z as Ordinal ; xz in rng xi by A10, A33, FUNCT_1:def_3; then A35: xz in sup xi by ORDINAL2:19; x9 in xz by A10, A21, A28, A33, A34, FUNCT_1:12; hence x in sup xi by A35, ORDINAL1:10; ::_thesis: verum end; end; end; hence x in sup xi ; ::_thesis: verum end; sup A = A by ORDINAL2:18; hence sup xi c= A by A3, ORDINAL2:22, RELAT_1:26; ::_thesis: verum end; theorem Th9: :: CARD_5:9 for A being Ordinal ex M being Cardinal st ( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds M c= B ) ) proof let A be Ordinal; ::_thesis: ex M being Cardinal st ( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds M c= B ) ) defpred S1[ Ordinal] means ( $1 c= card A & A is_cofinal_with $1 ); A1: ex B being Ordinal st S1[B] by Th8; consider C being Ordinal such that A2: S1[C] and A3: for B being Ordinal st S1[B] holds C c= B from ORDINAL1:sch_1(A1); take M = card C; ::_thesis: ( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds M c= B ) ) consider B being Ordinal such that A4: B c= M and A5: C is_cofinal_with B by Th8; A6: M c= C by CARD_1:8; then A7: B c= C by A4, XBOOLE_1:1; then B c= card A by A2, XBOOLE_1:1; then C c= B by A2, A3, A5, ORDINAL4:37; then A8: C = B by A7, XBOOLE_0:def_10; hence ( M c= card A & A is_cofinal_with M ) by A2, A4, A6, XBOOLE_0:def_10; ::_thesis: for B being Ordinal st A is_cofinal_with B holds M c= B let B be Ordinal; ::_thesis: ( A is_cofinal_with B implies M c= B ) assume that A9: A is_cofinal_with B and A10: not M c= B ; ::_thesis: contradiction A11: C = M by A4, A6, A8, XBOOLE_0:def_10; then not B c= card A by A3, A9, A10; hence contradiction by A2, A11, A10, XBOOLE_1:1; ::_thesis: verum end; Lm3: for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds for A being Ordinal st A in dom phi holds ( A in dom psi & phi . A = psi . A ) proof let phi, psi be Ordinal-Sequence; ::_thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies for A being Ordinal st A in dom phi holds ( A in dom psi & phi . A = psi . A ) ) assume that A1: rng phi = rng psi and A2: phi is increasing ; ::_thesis: ( not psi is increasing or for A being Ordinal st A in dom phi holds ( A in dom psi & phi . A = psi . A ) ) defpred S1[ Ordinal] means ( $1 in dom phi implies ( $1 in dom psi & phi . $1 = psi . $1 ) ); assume A3: for A, B being Ordinal st A in B & B in dom psi holds psi . A in psi . B ; :: according to ORDINAL2:def_12 ::_thesis: for A being Ordinal st A in dom phi holds ( A in dom psi & phi . A = psi . A ) A4: for A being Ordinal st ( for B being Ordinal st B in A holds S1[B] ) holds S1[A] proof let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds S1[B] ) implies S1[A] ) assume that A5: for B being Ordinal st B in A & B in dom phi holds ( B in dom psi & phi . B = psi . B ) and A6: A in dom phi ; ::_thesis: ( A in dom psi & phi . A = psi . A ) phi . A in rng phi by A6, FUNCT_1:def_3; then consider x being set such that A7: x in dom psi and A8: phi . A = psi . x by A1, FUNCT_1:def_3; reconsider x = x as Ordinal by A7; A9: now__::_thesis:_not_A_in_x assume A10: A in x ; ::_thesis: contradiction then A11: A in dom psi by A7, ORDINAL1:10; then psi . A in rng psi by FUNCT_1:def_3; then consider y being set such that A12: y in dom phi and A13: psi . A = phi . y by A1, FUNCT_1:def_3; reconsider y = y as Ordinal by A12; psi . A in psi . x by A3, A7, A10; then not A c= y by A2, A8, A12, A13, ORDINAL1:5, ORDINAL4:9; then A14: y in A by ORDINAL1:16; then A15: psi . y = phi . y by A5, A12; psi . y in psi . A by A3, A11, A14; hence contradiction by A13, A15; ::_thesis: verum end; now__::_thesis:_not_x_in_A assume A16: x in A ; ::_thesis: contradiction then ( phi . x in phi . A & x in dom phi ) by A2, A6, ORDINAL1:10, ORDINAL2:def_12; then phi . A in phi . A by A5, A8, A16; hence contradiction ; ::_thesis: verum end; hence ( A in dom psi & phi . A = psi . A ) by A7, A8, A9, ORDINAL1:14; ::_thesis: verum end; thus for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A4); ::_thesis: verum end; theorem :: CARD_5:10 for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds phi = psi proof let phi, psi be Ordinal-Sequence; ::_thesis: ( rng phi = rng psi & phi is increasing & psi is increasing implies phi = psi ) assume A1: ( rng phi = rng psi & phi is increasing & psi is increasing ) ; ::_thesis: phi = psi A2: dom phi = dom psi proof thus dom phi c= dom psi :: according to XBOOLE_0:def_10 ::_thesis: dom psi c= dom phi proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom phi or x in dom psi ) assume x in dom phi ; ::_thesis: x in dom psi hence x in dom psi by A1, Lm3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom psi or x in dom phi ) assume x in dom psi ; ::_thesis: x in dom phi hence x in dom phi by A1, Lm3; ::_thesis: verum end; for x being set st x in dom phi holds phi . x = psi . x by A1, Lm3; hence phi = psi by A2, FUNCT_1:2; ::_thesis: verum end; theorem Th11: :: CARD_5:11 for phi being Ordinal-Sequence st phi is increasing holds phi is one-to-one proof let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing implies phi is one-to-one ) assume A1: for A, B being Ordinal st A in B & B in dom phi holds phi . A in phi . B ; :: according to ORDINAL2:def_12 ::_thesis: phi is one-to-one let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom phi or not b1 in dom phi or not phi . x = phi . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom phi or not y in dom phi or not phi . x = phi . y or x = y ) assume that A2: ( x in dom phi & y in dom phi ) and A3: phi . x = phi . y ; ::_thesis: x = y reconsider A = x, B = y as Ordinal by A2; A4: ( A in B or A = B or B in A ) by ORDINAL1:14; not phi . A in phi . B by A3; hence x = y by A1, A2, A3, A4; ::_thesis: verum end; theorem Th12: :: CARD_5:12 for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi proof let phi, psi be Ordinal-Sequence; ::_thesis: (phi ^ psi) | (dom phi) = phi dom (phi ^ psi) = (dom phi) +^ (dom psi) by ORDINAL4:def_1; then dom phi c= dom (phi ^ psi) by ORDINAL3:24; then A1: dom phi = (dom (phi ^ psi)) /\ (dom phi) by XBOOLE_1:28; for x being set st x in dom phi holds phi . x = (phi ^ psi) . x by ORDINAL4:def_1; hence (phi ^ psi) | (dom phi) = phi by A1, FUNCT_1:46; ::_thesis: verum end; theorem :: CARD_5:13 for X being set for M being Cardinal st X <> {} holds card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) proof let X be set ; ::_thesis: for M being Cardinal st X <> {} holds card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) let M be Cardinal; ::_thesis: ( X <> {} implies card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) ) set Z = { Y where Y is Subset of X : card Y in M } ; X, card X are_equipotent by CARD_1:def_2; then consider f being Function such that A1: f is one-to-one and A2: dom f = X and A3: rng f = card X by WELLORD2:def_4; defpred S1[ set , set ] means ex A being Ordinal ex phi being Ordinal-Sequence st ( $2 = [A,phi] & dom phi = M & phi | A is increasing & rng (phi | A) = f .: $1 & ( for B being Ordinal st A c= B & B in M holds phi . B = {} ) ); A4: for x being set st x in { Y where Y is Subset of X : card Y in M } holds ex y being set st S1[x,y] proof deffunc H1( set ) -> set = {} ; let x be set ; ::_thesis: ( x in { Y where Y is Subset of X : card Y in M } implies ex y being set st S1[x,y] ) set A = order_type_of (RelIncl (f .: x)); consider xi2 being Ordinal-Sequence such that A5: ( dom xi2 = M -^ (order_type_of (RelIncl (f .: x))) & ( for B being Ordinal st B in M -^ (order_type_of (RelIncl (f .: x))) holds xi2 . B = H1(B) ) ) from ORDINAL2:sch_3(); assume x in { Y where Y is Subset of X : card Y in M } ; ::_thesis: ex y being set st S1[x,y] then A6: ex Y being Subset of X st ( x = Y & card Y in M ) ; consider xi1 being Ordinal-Sequence such that xi1 = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (f .: x)))),(RelIncl (f .: x))) and A7: xi1 is increasing and A8: dom xi1 = order_type_of (RelIncl (f .: x)) and A9: rng xi1 = f .: x by A3, Th5, RELAT_1:111; set phi = xi1 ^ xi2; take y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)]; ::_thesis: S1[x,y] take order_type_of (RelIncl (f .: x)) ; ::_thesis: ex phi being Ordinal-Sequence st ( y = [(order_type_of (RelIncl (f .: x))),phi] & dom phi = M & phi | (order_type_of (RelIncl (f .: x))) is increasing & rng (phi | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds phi . B = {} ) ) take xi1 ^ xi2 ; ::_thesis: ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x & ( for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds (xi1 ^ xi2) . B = {} ) ) card (f .: x) = card (order_type_of (RelIncl (f .: x))) by A3, Th7, RELAT_1:111; then card (order_type_of (RelIncl (f .: x))) in M by A6, CARD_1:67, ORDINAL1:12; then order_type_of (RelIncl (f .: x)) in M by CARD_3:44; then order_type_of (RelIncl (f .: x)) c= M by ORDINAL1:def_2; then (order_type_of (RelIncl (f .: x))) +^ (M -^ (order_type_of (RelIncl (f .: x)))) = M by ORDINAL3:def_5; hence ( y = [(order_type_of (RelIncl (f .: x))),(xi1 ^ xi2)] & dom (xi1 ^ xi2) = M & (xi1 ^ xi2) | (order_type_of (RelIncl (f .: x))) is increasing & rng ((xi1 ^ xi2) | (order_type_of (RelIncl (f .: x)))) = f .: x ) by A7, A8, A9, A5, Th12, ORDINAL4:def_1; ::_thesis: for B being Ordinal st order_type_of (RelIncl (f .: x)) c= B & B in M holds (xi1 ^ xi2) . B = {} let B be Ordinal; ::_thesis: ( order_type_of (RelIncl (f .: x)) c= B & B in M implies (xi1 ^ xi2) . B = {} ) assume that A10: order_type_of (RelIncl (f .: x)) c= B and A11: B in M ; ::_thesis: (xi1 ^ xi2) . B = {} A12: B -^ (order_type_of (RelIncl (f .: x))) in M -^ (order_type_of (RelIncl (f .: x))) by A10, A11, ORDINAL3:53; B = (order_type_of (RelIncl (f .: x))) +^ (B -^ (order_type_of (RelIncl (f .: x)))) by A10, ORDINAL3:def_5; then (xi1 ^ xi2) . B = xi2 . (B -^ (order_type_of (RelIncl (f .: x)))) by A8, A5, A12, ORDINAL4:def_1; hence (xi1 ^ xi2) . B = {} by A5, A12; ::_thesis: verum end; consider g being Function such that A13: ( dom g = { Y where Y is Subset of X : card Y in M } & ( for x being set st x in { Y where Y is Subset of X : card Y in M } holds S1[x,g . x] ) ) from CLASSES1:sch_1(A4); assume A14: X <> {} ; ::_thesis: card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) rng g c= [:M,(Funcs (M,(card X))):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in [:M,(Funcs (M,(card X))):] ) assume x in rng g ; ::_thesis: x in [:M,(Funcs (M,(card X))):] then consider y being set such that A15: y in dom g and A16: x = g . y by FUNCT_1:def_3; consider A being Ordinal, phi being Ordinal-Sequence such that A17: x = [A,phi] and A18: dom phi = M and A19: phi | A is increasing and A20: rng (phi | A) = f .: y and A21: for B being Ordinal st A c= B & B in M holds phi . B = {} by A13, A15, A16; A22: ex Y being Subset of X st ( y = Y & card Y in M ) by A13, A15; rng phi c= card X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in card X ) assume x in rng phi ; ::_thesis: x in card X then consider z being set such that A23: z in dom phi and A24: x = phi . z by FUNCT_1:def_3; reconsider z = z as Ordinal by A23; ( z in A or A c= z ) by ORDINAL1:16; then ( ( x in f .: y & f .: y c= card X ) or x = {} ) by A3, A18, A20, A21, A23, A24, FUNCT_1:50, RELAT_1:111; hence x in card X by A14, ORDINAL3:8; ::_thesis: verum end; then A25: phi in Funcs (M,(card X)) by A18, FUNCT_2:def_2; A26: ( A c= M or M c= A ) ; phi | A is one-to-one by A19, Th11; then dom (phi | A),f .: y are_equipotent by A20, WELLORD2:def_4; then card (dom (phi | A)) = card (f .: y) by CARD_1:5; then card (dom (phi | A)) in M by A22, CARD_1:67, ORDINAL1:12; then A27: dom (phi | A) in M by CARD_3:44; then dom (phi | A) <> M ; then A in M by A18, A27, A26, RELAT_1:62, RELAT_1:68; hence x in [:M,(Funcs (M,(card X))):] by A17, A25, ZFMISC_1:87; ::_thesis: verum end; then A28: card (rng g) c= card [:M,(Funcs (M,(card X))):] by CARD_1:11; g is one-to-one 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 that A29: x in dom g and A30: y in dom g and A31: g . x = g . y ; ::_thesis: x = y consider A2 being Ordinal, phi2 being Ordinal-Sequence such that A32: g . y = [A2,phi2] and dom phi2 = M and phi2 | A2 is increasing and A33: rng (phi2 | A2) = f .: y and for B being Ordinal st A2 c= B & B in M holds phi2 . B = {} by A13, A30; consider A1 being Ordinal, phi1 being Ordinal-Sequence such that A34: g . x = [A1,phi1] and dom phi1 = M and phi1 | A1 is increasing and A35: rng (phi1 | A1) = f .: x and for B being Ordinal st A1 c= B & B in M holds phi1 . B = {} by A13, A29; A36: ( A1 = A2 & phi1 = phi2 ) by A31, A34, A32, XTUPLE_0:1; A37: ex Y being Subset of X st ( x = Y & card Y in M ) by A13, A29; thus x c= y :: according to XBOOLE_0:def_10 ::_thesis: y c= x proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in y ) assume A38: z in x ; ::_thesis: z in y then f . z in f .: x by A2, A37, FUNCT_1:def_6; then ex x1 being set st ( x1 in dom f & x1 in y & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def_6; hence z in y by A1, A2, A37, A38, FUNCT_1:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in y or z in x ) A39: ex Y being Subset of X st ( y = Y & card Y in M ) by A13, A30; assume A40: z in y ; ::_thesis: z in x then f . z in f .: y by A2, A39, FUNCT_1:def_6; then ex x1 being set st ( x1 in dom f & x1 in x & f . z = f . x1 ) by A35, A33, A36, FUNCT_1:def_6; hence z in x by A1, A2, A39, A40, FUNCT_1:def_4; ::_thesis: verum end; then A41: { Y where Y is Subset of X : card Y in M } , rng g are_equipotent by A13, WELLORD2:def_4; card [:M,(Funcs (M,(card X))):] = card [:M,(card (Funcs (M,(card X)))):] by CARD_2:7 .= M *` (card (Funcs (M,(card X)))) by CARD_2:def_2 .= M *` (exp ((card X),M)) by CARD_2:def_3 ; hence card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M)) by A41, A28, CARD_1:5; ::_thesis: verum end; theorem Th14: :: CARD_5:14 for M being Cardinal holds M in exp (2,M) proof let M be Cardinal; ::_thesis: M in exp (2,M) ( card (bool M) = exp (2,(card M)) & card M = M ) by CARD_1:def_2, CARD_2:31; hence M in exp (2,M) by CARD_1:14; ::_thesis: verum end; registration cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for set ; existence ex b1 being Cardinal st b1 is infinite proof take omega ; ::_thesis: omega is infinite thus omega is infinite ; ::_thesis: verum end; end; registration cluster infinite -> non empty for set ; coherence for b1 being set st b1 is infinite holds not b1 is empty ; end; definition mode Aleph is infinite Cardinal; let M be Cardinal; func cf M -> Cardinal means :Def1: :: CARD_5:def 1 ( M is_cofinal_with it & ( for N being Cardinal st M is_cofinal_with N holds it c= N ) ); existence ex b1 being Cardinal st ( M is_cofinal_with b1 & ( for N being Cardinal st M is_cofinal_with N holds b1 c= N ) ) proof defpred S1[ Ordinal] means ( M is_cofinal_with $1 & $1 is Cardinal ); A1: ex A being Ordinal st S1[A] ; consider A being Ordinal such that A2: ( S1[A] & ( for B being Ordinal st S1[B] holds A c= B ) ) from ORDINAL1:sch_1(A1); reconsider K = A as Cardinal by A2; take K ; ::_thesis: ( M is_cofinal_with K & ( for N being Cardinal st M is_cofinal_with N holds K c= N ) ) thus M is_cofinal_with K by A2; ::_thesis: for N being Cardinal st M is_cofinal_with N holds K c= N let N be Cardinal; ::_thesis: ( M is_cofinal_with N implies K c= N ) assume M is_cofinal_with N ; ::_thesis: K c= N hence K c= N by A2; ::_thesis: verum end; uniqueness for b1, b2 being Cardinal st M is_cofinal_with b1 & ( for N being Cardinal st M is_cofinal_with N holds b1 c= N ) & M is_cofinal_with b2 & ( for N being Cardinal st M is_cofinal_with N holds b2 c= N ) holds b1 = b2 proof let K1, K2 be Cardinal; ::_thesis: ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds K2 c= N ) implies K1 = K2 ) assume ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds K2 c= N ) ) ; ::_thesis: K1 = K2 then ( K1 c= K2 & K2 c= K1 ) ; hence K1 = K2 by XBOOLE_0:def_10; ::_thesis: verum end; let N be Cardinal; funcN -powerfunc_of M -> Cardinal-Function means :Def2: :: CARD_5:def 2 ( ( for x being set holds ( x in dom it iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds it . K = exp (K,N) ) ); existence ex b1 being Cardinal-Function st ( ( for x being set holds ( x in dom b1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds b1 . K = exp (K,N) ) ) proof deffunc H1( set ) -> set = exp ((card $1),N); defpred S1[ set ] means $1 is Cardinal; consider X being set such that A3: for x being set holds ( x in X iff ( x in M & S1[x] ) ) from XBOOLE_0:sch_1(); consider f being Cardinal-Function such that A4: ( dom f = X & ( for x being set st x in X holds f . x = H1(x) ) ) from CARD_3:sch_1(); take f ; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds f . K = exp (K,N) ) ) thus for x being set holds ( x in dom f iff ( x in M & x is Cardinal ) ) by A3, A4; ::_thesis: for K being Cardinal st K in M holds f . K = exp (K,N) let K be Cardinal; ::_thesis: ( K in M implies f . K = exp (K,N) ) assume K in M ; ::_thesis: f . K = exp (K,N) then ( K = card K & K in X ) by A3, CARD_1:def_2; hence f . K = exp (K,N) by A4; ::_thesis: verum end; uniqueness for b1, b2 being Cardinal-Function st ( for x being set holds ( x in dom b1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds b1 . K = exp (K,N) ) & ( for x being set holds ( x in dom b2 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds b2 . K = exp (K,N) ) holds b1 = b2 proof defpred S1[ set ] means ( $1 in M & $1 is Cardinal ); let f1, f2 be Cardinal-Function; ::_thesis: ( ( for x being set holds ( x in dom f1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds f1 . K = exp (K,N) ) & ( for x being set holds ( x in dom f2 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds f2 . K = exp (K,N) ) implies f1 = f2 ) assume that A5: for x being set holds ( x in dom f1 iff S1[x] ) and A6: for K being Cardinal st K in M holds f1 . K = exp (K,N) and A7: for x being set holds ( x in dom f2 iff S1[x] ) and A8: for K being Cardinal st K in M holds f2 . K = exp (K,N) ; ::_thesis: f1 = f2 A9: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume A10: x in dom f1 ; ::_thesis: f1 . x = f2 . x then reconsider K = x as Cardinal by A5; A11: K in M by A5, A10; hence f1 . x = exp (K,N) by A6 .= f2 . x by A8, A11 ; ::_thesis: verum end; dom f1 = dom f2 from XBOOLE_0:sch_2(A5, A7); hence f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines cf CARD_5:def_1_:_ for M, b2 being Cardinal holds ( b2 = cf M iff ( M is_cofinal_with b2 & ( for N being Cardinal st M is_cofinal_with N holds b2 c= N ) ) ); :: deftheorem Def2 defines -powerfunc_of CARD_5:def_2_:_ for M, N being Cardinal for b3 being Cardinal-Function holds ( b3 = N -powerfunc_of M iff ( ( for x being set holds ( x in dom b3 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds b3 . K = exp (K,N) ) ) ); registration let A be Ordinal; cluster alef A -> infinite ; coherence not alef A is finite by Th3; end; begin theorem :: CARD_5:15 for a being Aleph ex A being Ordinal st a = alef A by Th4; theorem Th16: :: CARD_5:16 for n being Element of NAT for a being Aleph holds ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) proof let n be Element of NAT ; ::_thesis: for a being Aleph holds ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) let a be Aleph; ::_thesis: ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) ( omega c= a & card n in omega ) by CARD_3:85; hence ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) ; ::_thesis: verum end; theorem Th17: :: CARD_5:17 for M being Cardinal for a being Aleph st ( a c= M or a in M ) holds M is Aleph proof let M be Cardinal; ::_thesis: for a being Aleph st ( a c= M or a in M ) holds M is Aleph let a be Aleph; ::_thesis: ( ( a c= M or a in M ) implies M is Aleph ) assume A1: ( a c= M or a in M ) ; ::_thesis: M is Aleph omega c= a by Th16; then omega c= M by A1, XBOOLE_1:1; hence M is Aleph ; ::_thesis: verum end; theorem Th18: :: CARD_5:18 for M being Cardinal for a being Aleph st ( a c= M or a in M ) holds ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) proof let M be Cardinal; ::_thesis: for a being Aleph st ( a c= M or a in M ) holds ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) let a be Aleph; ::_thesis: ( ( a c= M or a in M ) implies ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) ) A1: card 0 in a by Th16; assume A2: ( a c= M or a in M ) ; ::_thesis: ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) then M is infinite by Th17; hence ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) by A2, A1, CARD_2:76, CARD_4:16; ::_thesis: verum end; theorem :: CARD_5:19 for a being Aleph holds ( a +` a = a & a *` a = a ) by CARD_2:75, CARD_4:15; theorem Th20: :: CARD_5:20 for M being Cardinal for a being Aleph holds M c= exp (M,a) proof let M be Cardinal; ::_thesis: for a being Aleph holds M c= exp (M,a) let a be Aleph; ::_thesis: M c= exp (M,a) 1 in a by Lm1, Th16; then ( ( M = 0 & {} c= exp (M,a) ) or ( exp (M,1) c= exp (M,a) & exp (M,1) = M ) ) by CARD_2:27, CARD_2:93, XBOOLE_1:2; hence M c= exp (M,a) ; ::_thesis: verum end; theorem :: CARD_5:21 for a being Aleph holds union a = a by ORDINAL1:def_6; registration let a be Aleph; let M be Cardinal; clustera +` M -> infinite ; coherence not a +` M is finite proof ( a c= M or M c= a ) ; then ( ( a +` M = M & M is Aleph ) or a +` M = a ) by Th18, CARD_2:76; hence not a +` M is finite ; ::_thesis: verum end; end; registration let M be Cardinal; let a be Aleph; clusterM +` a -> infinite ; coherence not M +` a is finite ; end; registration let a, b be Aleph; clustera *` b -> infinite ; coherence not a *` b is finite proof ( a c= b or b c= a ) ; hence not a *` b is finite by Th18; ::_thesis: verum end; cluster exp (a,b) -> infinite ; coherence not exp (a,b) is finite proof 1 in b by Lm1, Th16; then A1: exp (a,1) c= exp (a,b) by CARD_2:92; ( exp (a,1) = a & omega c= a ) by Th16, CARD_2:27; then omega c= exp (a,b) by A1, XBOOLE_1:1; hence not exp (a,b) is finite ; ::_thesis: verum end; end; begin definition let IT be Aleph; attrIT is regular means :: CARD_5:def 3 cf IT = IT; end; :: deftheorem defines regular CARD_5:def_3_:_ for IT being Aleph holds ( IT is regular iff cf IT = IT ); notation let IT be Aleph; antonym irregular IT for regular ; end; registration let a be Aleph; cluster nextcard a -> infinite ; coherence not nextcard a is finite proof a in nextcard a by CARD_1:18; then omega c= nextcard a ; hence not nextcard a is finite ; ::_thesis: verum end; end; theorem Th22: :: CARD_5:22 cf omega = omega proof defpred S1[ set , set ] means $2 c= $1; assume A1: cf omega <> omega ; ::_thesis: contradiction cf omega c= omega by Def1; then cf omega in omega by A1, CARD_1:3; then reconsider B = cf omega as finite set ; set n = card B; A2: for x, y being set st S1[x,y] & S1[y,x] holds x = y by XBOOLE_0:def_10; A3: for x, y, z being set st S1[x,y] & S1[y,z] holds S1[x,z] by XBOOLE_1:1; card (cf omega) = cf omega by CARD_1:def_2; then omega is_cofinal_with card B by Def1; then consider xi being Ordinal-Sequence such that A4: dom xi = card B and A5: rng xi c= omega and xi is increasing and A6: omega = sup xi by ORDINAL2:def_17; reconsider rxi = rng xi as finite set by A4, FINSET_1:8; A7: rxi <> {} by A6, ORDINAL2:18; consider x being set such that A8: ( x in rxi & ( for y being set st y in rxi & y <> x holds not S1[y,x] ) ) from CARD_2:sch_1(A7, A2, A3); reconsider x = x as Ordinal by A5, A8; now__::_thesis:_for_A_being_Ordinal_st_A_in_rng_xi_holds_ A_in_succ_x let A be Ordinal; ::_thesis: ( A in rng xi implies A in succ x ) assume A in rng xi ; ::_thesis: A in succ x then ( A c= x or not x c= A ) by A8; hence A in succ x by ORDINAL1:22; ::_thesis: verum end; then A9: omega c= succ x by A6, ORDINAL2:20; succ x in omega by A5, A8, ORDINAL1:28; hence contradiction by A9; ::_thesis: verum end; Lm4: 1 = card 1 by CARD_1:def_2; theorem Th23: :: CARD_5:23 for a being Aleph holds cf (nextcard a) = nextcard a proof let a be Aleph; ::_thesis: cf (nextcard a) = nextcard a nextcard a is_cofinal_with cf (nextcard a) by Def1; then consider xi being Ordinal-Sequence such that A1: dom xi = cf (nextcard a) and A2: rng xi c= nextcard a and xi is increasing and A3: nextcard a = sup xi by ORDINAL2:def_17; A4: ( card (Union xi) c= Sum (Card xi) & Sum ((cf (nextcard a)) --> a) = (cf (nextcard a)) *` a ) by CARD_2:65, CARD_3:39; A5: ( card (nextcard a) = nextcard a & succ (Union xi) = (Union xi) +^ 1 ) by CARD_1:def_2, ORDINAL2:31; A6: now__::_thesis:_for_x_being_set_st_x_in_cf_(nextcard_a)_holds_ (Card_xi)_._x_c=_((cf_(nextcard_a))_-->_a)_._x let x be set ; ::_thesis: ( x in cf (nextcard a) implies (Card xi) . x c= ((cf (nextcard a)) --> a) . x ) assume A7: x in cf (nextcard a) ; ::_thesis: (Card xi) . x c= ((cf (nextcard a)) --> a) . x xi . x in rng xi by A1, A7, FUNCT_1:def_3; then A8: card (xi . x) in nextcard a by A2, CARD_1:8, ORDINAL1:12; ( (Card xi) . x = card (xi . x) & ((cf (nextcard a)) --> a) . x = a ) by A1, A7, CARD_3:def_2, FUNCOP_1:7; hence (Card xi) . x c= ((cf (nextcard a)) --> a) . x by A8, CARD_3:91; ::_thesis: verum end; ( dom (Card xi) = dom xi & dom ((cf (nextcard a)) --> a) = cf (nextcard a) ) by CARD_3:def_2, FUNCOP_1:13; then Sum (Card xi) c= Sum ((cf (nextcard a)) --> a) by A1, A6, CARD_3:30; then card (Union xi) c= (cf (nextcard a)) *` a by A4, XBOOLE_1:1; then A9: (card (Union xi)) +` 1 c= ((cf (nextcard a)) *` a) +` 1 by CARD_2:84; A10: card ((Union xi) +^ 1) = (card (Union xi)) +` (card 1) by CARD_2:13; ex A being Ordinal st rng xi c= A by ORDINAL2:def_4; then On (rng xi) = rng xi by ORDINAL3:6; then A11: card (nextcard a) c= card (succ (Union xi)) by A3, CARD_1:11, ORDINAL3:72; A12: cf (nextcard a) c= nextcard a by Def1; now__::_thesis:_cf_(nextcard_a)_=_nextcard_a percases ( cf (nextcard a) = 0 or cf (nextcard a) <> 0 ) ; suppose cf (nextcard a) = 0 ; ::_thesis: cf (nextcard a) = nextcard a then A13: (cf (nextcard a)) *` a = 0 by CARD_2:20; ( 0 +` 1 = 1 & 1 in nextcard a ) by Lm1, Th16, CARD_2:18; hence cf (nextcard a) = nextcard a by A11, A5, A9, A10, A13, Lm4; ::_thesis: verum end; supposeA14: cf (nextcard a) <> 0 ; ::_thesis: cf (nextcard a) = nextcard a 0 c= cf (nextcard a) by XBOOLE_1:2; then A15: 0 in cf (nextcard a) by A14, CARD_1:3; A16: ( cf (nextcard a) c= a or a c= cf (nextcard a) ) ; 1 in a by Lm1, Th16; then A17: ( ( (cf (nextcard a)) *` a = a & a +` 1 = a & a in nextcard a ) or ( (cf (nextcard a)) *` a = cf (nextcard a) & cf (nextcard a) is Aleph ) ) by A15, A16, Th18, CARD_1:18, CARD_2:76, CARD_4:16; then ( nextcard a c= (cf (nextcard a)) +` 1 & 1 in cf (nextcard a) ) by A11, A5, A9, A10, Lm1, Th16, CARD_1:4, XBOOLE_1:1; then nextcard a c= cf (nextcard a) by A11, A5, A9, A10, A17, Lm1, CARD_1:4, CARD_2:76; hence cf (nextcard a) = nextcard a by A12, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence cf (nextcard a) = nextcard a ; ::_thesis: verum end; theorem Th24: :: CARD_5:24 for a being Aleph holds omega c= cf a proof let a be Aleph; ::_thesis: omega c= cf a A1: a is_cofinal_with cf a by Def1; then cf a <> {} by ORDINAL2:50; then A2: {} in cf a by ORDINAL3:8; cf a is limit_ordinal by A1, ORDINAL4:38; hence omega c= cf a by A2, ORDINAL1:def_11; ::_thesis: verum end; theorem :: CARD_5:25 for n being Element of NAT holds ( cf 0 = 0 & cf (card (n + 1)) = 1 ) proof let n be Element of NAT ; ::_thesis: ( cf 0 = 0 & cf (card (n + 1)) = 1 ) A1: succ n is_cofinal_with 1 by ORDINAL3:73; ( card (n + 1) = n + 1 & n + 1 = succ n ) by CARD_1:def_2, NAT_1:38; then cf (card (n + 1)) c= 1 by A1, Def1; then A2: ( cf (card (n + 1)) = 1 or ( cf (card (n + 1)) = 0 & {} c= n & n in succ n ) ) by ORDINAL1:6, ORDINAL3:16, XBOOLE_1:2; ( cf 0 c= 0 & 0 c= cf 0 ) by Def1, XBOOLE_1:2; hence cf 0 = 0 by XBOOLE_0:def_10; ::_thesis: cf (card (n + 1)) = 1 card (n + 1) is_cofinal_with cf (card (n + 1)) by Def1; hence cf (card (n + 1)) = 1 by A2, ORDINAL2:50; ::_thesis: verum end; theorem Th26: :: CARD_5:26 for X being set for M being Cardinal st X c= M & card X in cf M holds ( sup X in M & union X in M ) proof let X be set ; ::_thesis: for M being Cardinal st X c= M & card X in cf M holds ( sup X in M & union X in M ) let M be Cardinal; ::_thesis: ( X c= M & card X in cf M implies ( sup X in M & union X in M ) ) assume that A1: X c= M and A2: card X in cf M ; ::_thesis: ( sup X in M & union X in M ) set A = order_type_of (RelIncl X); A3: card (order_type_of (RelIncl X)) = card X by A1, Th7; consider N being Cardinal such that A4: N c= card (order_type_of (RelIncl X)) and A5: order_type_of (RelIncl X) is_cofinal_with N and for C being Ordinal st order_type_of (RelIncl X) is_cofinal_with C holds N c= C by Th9; sup X is_cofinal_with order_type_of (RelIncl X) by A1, Th6; then A6: sup X is_cofinal_with N by A5, ORDINAL4:37; A7: now__::_thesis:_not_sup_X_=_M assume sup X = M ; ::_thesis: contradiction then cf M c= N by A6, Def1; hence contradiction by A2, A3, A4, CARD_1:4; ::_thesis: verum end; for x being set st x in X holds x is Ordinal by A1; then reconsider A = union X as Ordinal by ORDINAL1:23; A8: sup M = M by ORDINAL2:18; sup X c= sup M by A1, ORDINAL2:22; then A9: sup X c< M by A8, A7, XBOOLE_0:def_8; hence sup X in M by ORDINAL1:11; ::_thesis: union X in M A c= sup X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup X ) assume x in A ; ::_thesis: x in sup X then consider Y being set such that A10: x in Y and A11: Y in X by TARSKI:def_4; reconsider Y = Y as Ordinal by A1, A11; Y in sup X by A11, ORDINAL2:19; then Y c= sup X by ORDINAL1:def_2; hence x in sup X by A10; ::_thesis: verum end; hence union X in M by A9, ORDINAL1:11, ORDINAL1:12; ::_thesis: verum end; theorem Th27: :: CARD_5:27 for M, N being Cardinal for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds ( sup phi in N & Union phi in N ) proof let M, N be Cardinal; ::_thesis: for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds ( sup phi in N & Union phi in N ) let phi be Ordinal-Sequence; ::_thesis: ( dom phi = M & rng phi c= N & M in cf N implies ( sup phi in N & Union phi in N ) ) assume that A1: dom phi = M and A2: rng phi c= N and A3: M in cf N ; ::_thesis: ( sup phi in N & Union phi in N ) A4: card M = M by CARD_1:def_2; card (rng phi) c= card M by A1, CARD_1:12; then card (rng phi) in cf N by A3, A4, ORDINAL1:12; hence ( sup phi in N & Union phi in N ) by A2, Th26; ::_thesis: verum end; registration let a be Aleph; cluster cf a -> infinite ; coherence not cf a is finite by Th17, Th24; end; theorem Th28: :: CARD_5:28 for a being Aleph st cf a in a holds a is limit_cardinal proof let a be Aleph; ::_thesis: ( cf a in a implies a is limit_cardinal ) assume A1: cf a in a ; ::_thesis: a is limit_cardinal given M being Cardinal such that A2: a = nextcard M ; :: according to CARD_1:def_4 ::_thesis: contradiction cf a c= M by A1, A2, CARD_3:91; then reconsider M = M as Aleph ; nextcard M in nextcard M by A1, A2, Th23; hence contradiction ; ::_thesis: verum end; theorem Th29: :: CARD_5:29 for a being Aleph st cf a in a holds ex xi being Ordinal-Sequence st ( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi ) proof let a be Aleph; ::_thesis: ( cf a in a implies ex xi being Ordinal-Sequence st ( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi ) ) a is_cofinal_with cf a by Def1; then consider xi being Ordinal-Sequence such that A1: dom xi = cf a and A2: rng xi c= a and xi is increasing and A3: a = sup xi by ORDINAL2:def_17; deffunc H1( T-Sequence) -> set = (nextcard (xi . (dom $1))) \/ (nextcard (sup $1)); consider phi being T-Sequence such that A4: ( dom phi = cf a & ( for A being Ordinal for psi being T-Sequence st A in cf a & psi = phi | A holds phi . A = H1(psi) ) ) from ORDINAL1:sch_4(); phi is Ordinal-yielding proof take sup (rng phi) ; :: according to ORDINAL2:def_4 ::_thesis: rng phi c= sup (rng phi) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in sup (rng phi) ) assume A5: x in rng phi ; ::_thesis: x in sup (rng phi) then consider y being set such that A6: y in dom phi and A7: x = phi . y by FUNCT_1:def_3; reconsider y = y as Ordinal by A6; y c= dom phi by A6, ORDINAL1:def_2; then dom (phi | y) = y by RELAT_1:62; then x = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A6, A7; hence x in sup (rng phi) by A5, ORDINAL2:19; ::_thesis: verum end; then reconsider phi = phi as Ordinal-Sequence ; defpred S1[ Ordinal] means ( $1 in cf a implies phi . $1 in a ); assume cf a in a ; ::_thesis: ex xi being Ordinal-Sequence st ( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi ) then A8: a is limit_cardinal by Th28; A9: now__::_thesis:_for_A_being_Ordinal_st_(_for_B_being_Ordinal_st_B_in_A_holds_ S1[B]_)_holds_ S1[A] let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds S1[B] ) implies S1[A] ) assume A10: for B being Ordinal st B in A holds S1[B] ; ::_thesis: S1[A] thus S1[A] ::_thesis: verum proof assume A11: A in cf a ; ::_thesis: phi . A in a then A12: card A in cf a by CARD_1:9; A c= dom phi by A4, A11, ORDINAL1:def_2; then A13: dom (phi | A) = A by RELAT_1:62; then phi . A = (nextcard (xi . A)) \/ (nextcard (sup (phi | A))) by A4, A11; then A14: ( phi . A = nextcard (xi . A) or phi . A = nextcard (sup (phi | A)) ) by ORDINAL3:12; A15: rng (phi | A) c= a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (phi | A) or x in a ) assume x in rng (phi | A) ; ::_thesis: x in a then consider y being set such that A16: y in dom (phi | A) and A17: x = (phi | A) . y by FUNCT_1:def_3; reconsider y = y as Ordinal by A16; ( x = phi . y & y in cf a ) by A11, A13, A16, A17, FUNCT_1:47, ORDINAL1:10; hence x in a by A10, A13, A16; ::_thesis: verum end; (phi | A) .: A = rng (phi | A) by A13, RELAT_1:113; then card (rng (phi | A)) in cf a by A12, CARD_1:67, ORDINAL1:12; then sup (rng (phi | A)) in a by A15, Th26; then card (sup (phi | A)) in a by CARD_1:9; then A18: nextcard (card (sup (phi | A))) c= a by CARD_3:90; xi . A in rng xi by A1, A11, FUNCT_1:def_3; then card (xi . A) in a by A2, CARD_1:9; then A19: nextcard (card (xi . A)) c= a by CARD_3:90; A20: ( nextcard (card (sup (phi | A))) <> a & nextcard (card (sup (phi | A))) = nextcard (sup (phi | A)) ) by A8, Th1, CARD_1:def_4; ( a <> nextcard (card (xi . A)) & nextcard (card (xi . A)) = nextcard (xi . A) ) by A8, Th1, CARD_1:def_4; hence phi . A in a by A19, A18, A20, A14, CARD_1:3; ::_thesis: verum end; end; A21: for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A9); A22: rng phi c= a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in a ) assume x in rng phi ; ::_thesis: x in a then ex y being set st ( y in dom phi & x = phi . y ) by FUNCT_1:def_3; hence x in a by A4, A21; ::_thesis: verum end; take phi ; ::_thesis: ( dom phi = cf a & rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi ) thus dom phi = cf a by A4; ::_thesis: ( rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi ) thus rng phi c= a ::_thesis: ( phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in a ) assume x in rng phi ; ::_thesis: x in a then ex y being set st ( y in dom phi & x = phi . y ) by FUNCT_1:def_3; hence x in a by A4, A21; ::_thesis: verum end; thus phi is increasing ::_thesis: ( a = sup phi & phi is Cardinal-Function & not 0 in rng phi ) 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 that A23: A in B and A24: B in dom phi ; ::_thesis: phi . A in phi . B reconsider C = phi . A as Ordinal ; A in dom phi by A23, A24, ORDINAL1:10; then C in rng (phi | B) by A23, FUNCT_1:50; then A25: C in sup (phi | B) by ORDINAL2:19; sup (phi | B) in nextcard (sup (phi | B)) by CARD_1:18; then A26: C in nextcard (sup (phi | B)) by A25, ORDINAL1:10; phi . B = (nextcard (xi . (dom (phi | B)))) \/ (nextcard (sup (phi | B))) by A4, A24; hence phi . A in phi . B by A26, XBOOLE_0:def_3; ::_thesis: verum end; thus a c= sup phi :: according to XBOOLE_0:def_10 ::_thesis: ( sup phi c= a & phi is Cardinal-Function & not 0 in rng phi ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in sup phi ) assume x in a ; ::_thesis: x in sup phi then reconsider x = x as Element of a ; consider A being Ordinal such that A27: A in rng xi and A28: x c= A by A3, ORDINAL2:21; consider y being set such that A29: y in dom xi and A30: A = xi . y by A27, FUNCT_1:def_3; reconsider y = y as Ordinal by A29; y c= cf a by A1, A29, ORDINAL1:def_2; then dom (phi | y) = y by A4, RELAT_1:62; then ( A in nextcard A & phi . y = (nextcard A) \/ (nextcard (sup (phi | y))) ) by A1, A4, A29, A30, CARD_1:18; then A in phi . y by XBOOLE_0:def_3; then A31: A c= phi . y by ORDINAL1:def_2; phi . y in rng phi by A1, A4, A29, FUNCT_1:def_3; then phi . y in sup phi by ORDINAL2:19; hence x in sup phi by A28, A31, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum end; sup a = a by ORDINAL2:18; hence sup phi c= a by A22, ORDINAL2:22; ::_thesis: ( phi is Cardinal-Function & not 0 in rng phi ) phi is Cardinal-yielding proof let y be set ; :: according to CARD_3:def_1 ::_thesis: ( not y in dom phi or phi . y is set ) assume A32: y in dom phi ; ::_thesis: phi . y is set then reconsider y = y as Ordinal ; y c= dom phi by A32, ORDINAL1:def_2; then dom (phi | y) = y by RELAT_1:62; then phi . y = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A32; hence phi . y is set by ORDINAL3:12; ::_thesis: verum end; hence phi is Cardinal-Function ; ::_thesis: not 0 in rng phi assume 0 in rng phi ; ::_thesis: contradiction then consider x being set such that A33: x in dom phi and A34: 0 = phi . x by FUNCT_1:def_3; reconsider x = x as Ordinal by A33; x c= dom phi by A33, ORDINAL1:def_2; then dom (phi | x) = x by RELAT_1:62; then 0 = (nextcard (xi . x)) \/ (nextcard (sup (phi | x))) by A4, A33, A34; then ( 0 = nextcard (xi . x) or 0 = nextcard (sup (phi | x)) ) ; hence contradiction by CARD_1:15; ::_thesis: verum end; theorem :: CARD_5:30 for a being Aleph holds ( omega is regular & nextcard a is regular ) proof let a be Aleph; ::_thesis: ( omega is regular & nextcard a is regular ) thus cf omega = omega by Th22; :: according to CARD_5:def_3 ::_thesis: nextcard a is regular thus cf (nextcard a) = nextcard a by Th23; :: according to CARD_5:def_3 ::_thesis: verum end; begin theorem Th31: :: CARD_5:31 for a, b being Aleph st a c= b holds exp (a,b) = exp (2,b) proof let a, b be Aleph; ::_thesis: ( a c= b implies exp (a,b) = exp (2,b) ) A1: card (bool a) = exp (2,(card a)) by CARD_2:31; ( card a = a & card a in card (bool a) ) by CARD_1:14, CARD_1:def_2; then A2: exp (a,b) c= exp ((exp (2,a)),b) by A1, CARD_2:92; assume a c= b ; ::_thesis: exp (a,b) = exp (2,b) then A3: ( exp ((exp (2,a)),b) = exp (2,(a *` b)) & a *` b = b ) by Th18, CARD_2:30; 2 in a by Lm2, Th16; then exp (2,b) c= exp (a,b) by CARD_2:92; hence exp (a,b) = exp (2,b) by A2, A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CARD_5:32 for a, b being Aleph holds exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) proof let a, b be Aleph; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) now__::_thesis:_exp_((nextcard_a),b)_=_(exp_(a,b))_*`_(nextcard_a) percases ( a in b or b c= a ) by CARD_1:4; supposeA1: a in b ; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) then a c= b by CARD_1:3; then A2: exp (a,b) = exp (2,b) by Th31; nextcard a c= b by A1, CARD_3:90; then ( exp ((nextcard a),b) = exp (2,b) & nextcard a in exp (2,b) ) by Th14, Th31, ORDINAL1:12; hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A2, Th18; ::_thesis: verum end; supposeA3: b c= a ; ::_thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) deffunc H1( Ordinal) -> set = Funcs (b,$1); consider phi being T-Sequence such that A4: ( dom phi = nextcard a & ( for A being Ordinal st A in nextcard a holds phi . A = H1(A) ) ) from ORDINAL2:sch_2(); A5: cf (nextcard a) = nextcard a by Th23; A6: b in nextcard a by A3, CARD_3:91; Funcs (b,(nextcard a)) c= Union phi proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (b,(nextcard a)) or x in Union phi ) assume x in Funcs (b,(nextcard a)) ; ::_thesis: x in Union phi then consider f being Function such that A7: x = f and A8: dom f = b and A9: rng f c= nextcard a by FUNCT_2:def_2; reconsider f = f as T-Sequence by A8, ORDINAL1:def_7; reconsider f = f as Ordinal-Sequence by A9, ORDINAL2:def_4; sup f in nextcard a by A6, A5, A8, A9, Th27; then A10: phi . (sup f) in rng phi by A4, FUNCT_1:def_3; rng f c= sup f by ORDINAL2:49; then A11: f in Funcs (b,(sup f)) by A8, FUNCT_2:def_2; phi . (sup f) = Funcs (b,(sup f)) by A6, A5, A4, A8, A9, Th27; hence x in Union phi by A7, A11, A10, TARSKI:def_4; ::_thesis: verum end; then A12: card (Funcs (b,(nextcard a))) c= card (Union phi) by CARD_1:11; ( card (Funcs (b,(nextcard a))) = exp ((nextcard a),b) & card (Union phi) c= Sum (Card phi) ) by CARD_2:def_3, CARD_3:39; then A13: exp ((nextcard a),b) c= Sum (Card phi) by A12, XBOOLE_1:1; a in nextcard a by CARD_1:18; then A14: ( (exp ((nextcard a),b)) *` (exp ((nextcard a),b)) = exp ((nextcard a),b) & exp (a,b) c= exp ((nextcard a),b) ) by CARD_2:92, CARD_4:15; ( exp ((nextcard a),1) = nextcard a & 1 in b ) by Lm1, Th16, CARD_2:27; then nextcard a c= exp ((nextcard a),b) by CARD_2:92; then A15: (exp (a,b)) *` (nextcard a) c= exp ((nextcard a),b) by A14, CARD_2:90; A16: now__::_thesis:_for_x_being_set_st_x_in_nextcard_a_holds_ (Card_phi)_._x_c=_((nextcard_a)_-->_(exp_(a,b)))_._x let x be set ; ::_thesis: ( x in nextcard a implies (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x ) A17: ( card (card x) = card x & card b = card b ) ; assume A18: x in nextcard a ; ::_thesis: (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x then reconsider x9 = x as Ordinal ; A19: phi . x9 = Funcs (b,x9) by A4, A18; card x in nextcard a by A18, CARD_1:8, ORDINAL1:12; then card x c= a by CARD_3:91; then Funcs (b,(card x)) c= Funcs (b,a) by FUNCT_5:56; then A20: card (Funcs (b,(card x))) c= card (Funcs (b,a)) by CARD_1:11; A21: card (Funcs (b,a)) = exp (a,b) by CARD_2:def_3; ( ((nextcard a) --> (exp (a,b))) . x = exp (a,b) & (Card phi) . x = card (phi . x) ) by A4, A18, CARD_3:def_2, FUNCOP_1:7; hence (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x by A19, A17, A20, A21, FUNCT_5:61; ::_thesis: verum end; ( dom (Card phi) = dom phi & dom ((nextcard a) --> (exp (a,b))) = nextcard a ) by CARD_3:def_2, FUNCOP_1:13; then A22: Sum (Card phi) c= Sum ((nextcard a) --> (exp (a,b))) by A4, A16, CARD_3:30; Sum ((nextcard a) --> (exp (a,b))) = (nextcard a) *` (exp (a,b)) by CARD_2:65; then exp ((nextcard a),b) c= (exp (a,b)) *` (nextcard a) by A13, A22, XBOOLE_1:1; hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A15, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) ; ::_thesis: verum end; theorem Th33: :: CARD_5:33 for b, a being Aleph holds Sum (b -powerfunc_of a) c= exp (a,b) proof let b, a be Aleph; ::_thesis: Sum (b -powerfunc_of a) c= exp (a,b) set X = { c where c is Element of a : c is Cardinal } ; set f = { c where c is Element of a : c is Cardinal } --> (exp (a,b)); { c where c is Element of a : c is Cardinal } c= a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of a : c is Cardinal } or x in a ) assume x in { c where c is Element of a : c is Cardinal } ; ::_thesis: x in a then ex c being Element of a st ( x = c & c is Cardinal ) ; hence x in a ; ::_thesis: verum end; then A1: { c where c is Element of a : c is Cardinal } --> (exp (a,b)) c= a --> (exp (a,b)) by FUNCT_4:4; Sum (a --> (exp (a,b))) = a *` (exp (a,b)) by CARD_2:65; then A2: Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) c= a *` (exp (a,b)) by A1, CARD_3:33; A3: ( dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } & dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal } ) proof thus dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } by FUNCOP_1:13; ::_thesis: dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal } thus dom (b -powerfunc_of a) c= { c where c is Element of a : c is Cardinal } :: according to XBOOLE_0:def_10 ::_thesis: { c where c is Element of a : c is Cardinal } c= dom (b -powerfunc_of a) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (b -powerfunc_of a) or x in { c where c is Element of a : c is Cardinal } ) assume x in dom (b -powerfunc_of a) ; ::_thesis: x in { c where c is Element of a : c is Cardinal } then ( x in a & x is Cardinal ) by Def2; hence x in { c where c is Element of a : c is Cardinal } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of a : c is Cardinal } or x in dom (b -powerfunc_of a) ) assume x in { c where c is Element of a : c is Cardinal } ; ::_thesis: x in dom (b -powerfunc_of a) then ex c being Element of a st ( x = c & c is Cardinal ) ; hence x in dom (b -powerfunc_of a) by Def2; ::_thesis: verum end; ( 1 in b & exp (a,1) = a ) by Lm1, Th16, CARD_2:27; then a c= exp (a,b) by CARD_2:93; then A4: a *` (exp (a,b)) = exp (a,b) by Th18; now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_a_:_c_is_Cardinal__}__holds_ (b_-powerfunc_of_a)_._x_c=_(_{__c_where_c_is_Element_of_a_:_c_is_Cardinal__}__-->_(exp_(a,b)))_._x let x be set ; ::_thesis: ( x in { c where c is Element of a : c is Cardinal } implies (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x ) assume A5: x in { c where c is Element of a : c is Cardinal } ; ::_thesis: (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x then consider c being Element of a such that A6: x = c and A7: c is Cardinal ; reconsider c = c as Cardinal by A7; A8: ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x = exp (a,b) by A5, FUNCOP_1:7; (b -powerfunc_of a) . x = exp (c,b) by A6, Def2; hence (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x by A8, CARD_2:93; ::_thesis: verum end; then Sum (b -powerfunc_of a) c= Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) by A3, CARD_3:30; hence Sum (b -powerfunc_of a) c= exp (a,b) by A2, A4, XBOOLE_1:1; ::_thesis: verum end; theorem :: CARD_5:34 for a, b being Aleph st a is limit_cardinal & b in cf a holds exp (a,b) = Sum (b -powerfunc_of a) proof let a, b be Aleph; ::_thesis: ( a is limit_cardinal & b in cf a implies exp (a,b) = Sum (b -powerfunc_of a) ) assume that A1: a is limit_cardinal and A2: b in cf a ; ::_thesis: exp (a,b) = Sum (b -powerfunc_of a) deffunc H1( Ordinal) -> set = Funcs (b,$1); consider L being T-Sequence such that A3: ( dom L = a & ( for A being Ordinal st A in a holds L . A = H1(A) ) ) from ORDINAL2:sch_2(); A4: now__::_thesis:_for_x_being_set_st_x_in_a_holds_ (Card_L)_._x_c=_(a_-->_(Sum_(b_-powerfunc_of_a)))_._x let x be set ; ::_thesis: ( x in a implies (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x ) A5: card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) by CARD_3:40; assume A6: x in a ; ::_thesis: (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x then reconsider x9 = x as Ordinal ; set m = card x9; A7: card x9 in a by A6, CARD_1:8, ORDINAL1:12; then card x9 in dom (b -powerfunc_of a) by Def2; then A8: (b -powerfunc_of a) . (card x) in rng (b -powerfunc_of a) by FUNCT_1:def_3; x9, card x9 are_equipotent by CARD_1:def_2; then A9: card (Funcs (b,x9)) = card (Funcs (b,(card x9))) by FUNCT_5:60; ( L . x = Funcs (b,x9) & (Card L) . x = card (L . x) ) by A3, A6, CARD_3:def_2; then A10: (Card L) . x = exp ((card x9),b) by A9, CARD_2:def_3; (b -powerfunc_of a) . (card x) = exp ((card x),b) by A7, Def2; then card (exp ((card x),b)) c= card (Union (b -powerfunc_of a)) by A8, CARD_1:11, ZFMISC_1:74; then A11: card (exp ((card x),b)) c= Sum (b -powerfunc_of a) by A5, XBOOLE_1:1; card (exp ((card x),b)) = exp ((card x),b) by CARD_1:def_2; hence (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x by A6, A10, A11, FUNCOP_1:7; ::_thesis: verum end; ( dom (a --> (Sum (b -powerfunc_of a))) = a & dom (Card L) = dom L ) by CARD_3:def_2, FUNCOP_1:13; then A12: Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a))) by A3, A4, CARD_3:30; a c= Sum (b -powerfunc_of a) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in Sum (b -powerfunc_of a) ) assume A13: x in a ; ::_thesis: x in Sum (b -powerfunc_of a) then reconsider x9 = x as Ordinal ; set m = card x9; card x9 in a by A13, CARD_1:8, ORDINAL1:12; then A14: nextcard (card x9) c= a by CARD_3:90; nextcard (card x9) <> a by A1, CARD_1:def_4; then A15: nextcard (card x9) in a by A14, CARD_1:3; then nextcard (card x9) in dom (b -powerfunc_of a) by Def2; then A16: (b -powerfunc_of a) . (nextcard (card x9)) in rng (b -powerfunc_of a) by FUNCT_1:def_3; (b -powerfunc_of a) . (nextcard (card x9)) = exp ((nextcard (card x9)),b) by A15, Def2; then A17: card (exp ((nextcard (card x9)),b)) c= card (Union (b -powerfunc_of a)) by A16, CARD_1:11, ZFMISC_1:74; A18: nextcard (card x9) c= exp ((nextcard (card x9)),b) by Th20; card x = card (card x) ; then A19: ( x9 in nextcard x9 & nextcard (card x) = nextcard x ) by CARD_1:18, CARD_3:88; ( card (exp ((nextcard (card x9)),b)) = exp ((nextcard (card x9)),b) & card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) ) by CARD_1:def_2, CARD_3:40; then exp ((nextcard (card x9)),b) c= Sum (b -powerfunc_of a) by A17, XBOOLE_1:1; then nextcard (card x) c= Sum (b -powerfunc_of a) by A18, XBOOLE_1:1; hence x in Sum (b -powerfunc_of a) by A19; ::_thesis: verum end; then A20: a *` (Sum (b -powerfunc_of a)) = Sum (b -powerfunc_of a) by Th18; Funcs (b,a) c= Union L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (b,a) or x in Union L ) assume x in Funcs (b,a) ; ::_thesis: x in Union L then consider f being Function such that A21: x = f and A22: dom f = b and A23: rng f c= a by FUNCT_2:def_2; reconsider f = f as T-Sequence by A22, ORDINAL1:def_7; reconsider f = f as Ordinal-Sequence by A23, ORDINAL2:def_4; rng f c= sup f by ORDINAL2:49; then A24: x in Funcs (b,(sup f)) by A21, A22, FUNCT_2:def_2; sup f in a by A2, A22, A23, Th27; then A25: L . (sup f) in rng L by A3, FUNCT_1:def_3; L . (sup f) = Funcs (b,(sup f)) by A2, A3, A22, A23, Th27; hence x in Union L by A24, A25, TARSKI:def_4; ::_thesis: verum end; then A26: card (Funcs (b,a)) c= card (Union L) by CARD_1:11; card (Union L) c= Sum (Card L) by CARD_3:39; then card (Funcs (b,a)) c= Sum (Card L) by A26, XBOOLE_1:1; then A27: exp (a,b) c= Sum (Card L) by CARD_2:def_3; A28: Sum (b -powerfunc_of a) c= exp (a,b) by Th33; Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a)) by CARD_2:65; then exp (a,b) c= a *` (Sum (b -powerfunc_of a)) by A27, A12, XBOOLE_1:1; hence exp (a,b) = Sum (b -powerfunc_of a) by A28, A20, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CARD_5:35 for a, b being Aleph st cf a c= b & b in a holds exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) proof let a, b be Aleph; ::_thesis: ( cf a c= b & b in a implies exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) ) assume that A1: cf a c= b and A2: b in a ; ::_thesis: exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) consider phi being Ordinal-Sequence such that A3: dom phi = cf a and A4: rng phi c= a and phi is increasing and A5: a = sup phi and A6: phi is Cardinal-Function and A7: not 0 in rng phi by A1, A2, Th29, ORDINAL1:12; defpred S1[ set , set ] means ex g, h being Function st ( g = $1 & h = $2 & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds ex fx being Function st ( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ); A8: for x being set st x in Funcs (b,a) holds ex x1 being set st S1[x,x1] proof let x be set ; ::_thesis: ( x in Funcs (b,a) implies ex x1 being set st S1[x,x1] ) assume x in Funcs (b,a) ; ::_thesis: ex x1 being set st S1[x,x1] then consider g being Function such that A9: ( x = g & dom g = b & rng g c= a ) by FUNCT_2:def_2; defpred S2[ set , set ] means ex fx being Function st ( $2 = [fx,(phi . $1)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . $1 implies fx . z = g . z ) & ( not g . z in phi . $1 implies fx . z = 0 ) ) ) ); A10: for y being set st y in cf a holds ex x2 being set st S2[y,x2] proof deffunc H1( set ) -> Element of NAT = 0 ; deffunc H2( set ) -> set = g . $1; let y be set ; ::_thesis: ( y in cf a implies ex x2 being set st S2[y,x2] ) assume y in cf a ; ::_thesis: ex x2 being set st S2[y,x2] defpred S3[ set ] means g . $1 in phi . y; consider fx being Function such that A11: ( dom fx = b & ( for z being set st z in b holds ( ( S3[z] implies fx . z = H2(z) ) & ( not S3[z] implies fx . z = H1(z) ) ) ) ) from PARTFUN1:sch_1(); take [fx,(phi . y)] ; ::_thesis: S2[y,[fx,(phi . y)]] take fx ; ::_thesis: ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) thus ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) by A11; ::_thesis: verum end; consider h being Function such that A12: ( dom h = cf a & ( for y being set st y in cf a holds S2[y,h . y] ) ) from CLASSES1:sch_1(A10); take h ; ::_thesis: S1[x,h] take g ; ::_thesis: ex h being Function st ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds ex fx being Function st ( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) take h ; ::_thesis: ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds ex fx being Function st ( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) thus ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds ex fx being Function st ( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) by A9, A12; ::_thesis: verum end; consider f being Function such that A13: ( dom f = Funcs (b,a) & ( for x being set st x in Funcs (b,a) holds S1[x,f . x] ) ) from CLASSES1:sch_1(A8); deffunc H1( set ) -> set = Funcs (b,$1); consider F being Function such that A14: ( dom F = dom (b -powerfunc_of a) & ( for x being set st x in dom (b -powerfunc_of a) holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); A15: rng f c= Funcs ((cf a),(Union (disjoin F))) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs ((cf a),(Union (disjoin F))) ) assume y in rng f ; ::_thesis: y in Funcs ((cf a),(Union (disjoin F))) then consider x being set such that A16: x in dom f and A17: y = f . x by FUNCT_1:def_3; consider g, h being Function such that g = x and A18: h = f . x and dom g = b and rng g c= a and A19: dom h = cf a and A20: for y being set st y in cf a holds ex fx being Function st ( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds ( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) by A13, A16; rng h c= Union (disjoin F) proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in rng h or x1 in Union (disjoin F) ) assume x1 in rng h ; ::_thesis: x1 in Union (disjoin F) then consider x2 being set such that A21: x2 in dom h and A22: x1 = h . x2 by FUNCT_1:def_3; consider fx being Function such that A23: x1 = [fx,(phi . x2)] and A24: dom fx = b and A25: for z being set st z in b holds ( ( g . z in phi . x2 implies fx . z = g . z ) & ( not g . z in phi . x2 implies fx . z = 0 ) ) by A19, A20, A21, A22; rng fx c= phi . x2 proof reconsider x2 = x2 as Ordinal by A19, A21; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng fx or z in phi . x2 ) reconsider A = phi . x2 as Ordinal ; assume z in rng fx ; ::_thesis: z in phi . x2 then consider z9 being set such that A26: ( z9 in dom fx & z = fx . z9 ) by FUNCT_1:def_3; A27: ( ( z = g . z9 & g . z9 in phi . x2 ) or z = 0 ) by A24, A25, A26; A <> 0 by A3, A7, A19, A21, FUNCT_1:def_3; hence z in phi . x2 by A27, ORDINAL3:8; ::_thesis: verum end; then A28: fx in Funcs (b,(phi . x2)) by A24, FUNCT_2:def_2; A29: ( [fx,(phi . x2)] `1 = fx & [fx,(phi . x2)] `2 = phi . x2 ) ; ( phi . x2 in rng phi & phi . x2 is Cardinal ) by A3, A6, A19, A21, CARD_3:def_1, FUNCT_1:def_3; then A30: phi . x2 in dom (b -powerfunc_of a) by A4, Def2; then F . (phi . x2) = Funcs (b,(phi . x2)) by A14; hence x1 in Union (disjoin F) by A14, A23, A28, A30, A29, CARD_3:22; ::_thesis: verum end; hence y in Funcs ((cf a),(Union (disjoin F))) by A17, A18, A19, FUNCT_2:def_2; ::_thesis: verum end; ( card (card (Union (disjoin F))) = card (Union (disjoin F)) & card (cf a) = cf a ) by CARD_1:def_2; then A31: card (Funcs ((cf a),(Union (disjoin F)))) = card (Funcs ((cf a),(card (Union (disjoin F))))) by FUNCT_5:61 .= exp ((card (Union (disjoin F))),(cf a)) by CARD_2:def_3 ; A32: dom (Card F) = dom F by CARD_3:def_2; A33: f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A34: x in dom f and A35: y in dom f and A36: f . x = f . y ; ::_thesis: x = y consider g1, h1 being Function such that A37: g1 = x and A38: h1 = f . x and A39: dom g1 = b and A40: rng g1 c= a and dom h1 = cf a and A41: for x1 being set st x1 in cf a holds ex fx being Function st ( h1 . x1 = [fx,(phi . x1)] & dom fx = b & ( for z being set st z in b holds ( ( g1 . z in phi . x1 implies fx . z = g1 . z ) & ( not g1 . z in phi . x1 implies fx . z = 0 ) ) ) ) by A13, A34; consider g2, h2 being Function such that A42: g2 = y and A43: h2 = f . y and A44: dom g2 = b and A45: rng g2 c= a and dom h2 = cf a and A46: for x2 being set st x2 in cf a holds ex fx being Function st ( h2 . x2 = [fx,(phi . x2)] & dom fx = b & ( for z being set st z in b holds ( ( g2 . z in phi . x2 implies fx . z = g2 . z ) & ( not g2 . z in phi . x2 implies fx . z = 0 ) ) ) ) by A13, A35; now__::_thesis:_for_x1_being_set_st_x1_in_b_holds_ g1_._x1_=_g2_._x1 let x1 be set ; ::_thesis: ( x1 in b implies g1 . x1 = g2 . x1 ) assume x1 in b ; ::_thesis: g1 . x1 = g2 . x1 then reconsider X = x1 as Element of b ; ( g1 . X in rng g1 & g2 . X in rng g2 ) by A39, A44, FUNCT_1:def_3; then reconsider A1 = g1 . x1, A2 = g2 . x1 as Element of a by A40, A45; set A = A1 \/ A2; ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12; then succ (A1 \/ A2) in a by ORDINAL1:28; then consider B being Ordinal such that A47: B in rng phi and A48: succ (A1 \/ A2) c= B by A5, ORDINAL2:21; consider x2 being set such that A49: x2 in dom phi and A50: B = phi . x2 by A47, FUNCT_1:def_3; A51: A1 \/ A2 in succ (A1 \/ A2) by ORDINAL1:6; then A52: A2 in B by A48, ORDINAL1:12, XBOOLE_1:7; consider f1 being Function such that A53: h1 . x2 = [f1,(phi . x2)] and dom f1 = b and A54: for z being set st z in b holds ( ( g1 . z in phi . x2 implies f1 . z = g1 . z ) & ( not g1 . z in phi . x2 implies f1 . z = 0 ) ) by A3, A41, A49; A1 in B by A48, A51, ORDINAL1:12, XBOOLE_1:7; then A55: f1 . X = g1 . x1 by A50, A54; consider f2 being Function such that A56: h2 . x2 = [f2,(phi . x2)] and dom f2 = b and A57: for z being set st z in b holds ( ( g2 . z in phi . x2 implies f2 . z = g2 . z ) & ( not g2 . z in phi . x2 implies f2 . z = 0 ) ) by A3, A46, A49; f1 = f2 by A36, A38, A43, A53, A56, XTUPLE_0:1; hence g1 . x1 = g2 . x1 by A50, A57, A52, A55; ::_thesis: verum end; hence x = y by A37, A39, A42, A44, FUNCT_1:2; ::_thesis: verum end; A58: dom (disjoin F) = dom F by CARD_3:def_3; A59: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (Card_(disjoin_F))_._x_=_(Card_F)_._x let x be set ; ::_thesis: ( x in dom F implies (Card (disjoin F)) . x = (Card F) . x ) assume A60: x in dom F ; ::_thesis: (Card (disjoin F)) . x = (Card F) . x then A61: (disjoin F) . x = [:(F . x),{x}:] by CARD_3:def_3; ( (Card F) . x = card (F . x) & (Card (disjoin F)) . x = card ((disjoin F) . x) ) by A58, A60, CARD_3:def_2; hence (Card (disjoin F)) . x = (Card F) . x by A61, CARD_1:69; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (Card_F)_._x_=_(b_-powerfunc_of_a)_._x let x be set ; ::_thesis: ( x in dom F implies (Card F) . x = (b -powerfunc_of a) . x ) assume A62: x in dom F ; ::_thesis: (Card F) . x = (b -powerfunc_of a) . x then reconsider M = x as Cardinal by A14, Def2; M in a by A14, A62, Def2; then A63: (b -powerfunc_of a) . M = exp (M,b) by Def2; ( (Card F) . x = card (F . x) & F . x = Funcs (b,x) ) by A14, A62, CARD_3:def_2; hence (Card F) . x = (b -powerfunc_of a) . x by A63, CARD_2:def_3; ::_thesis: verum end; then A64: Card F = b -powerfunc_of a by A14, A32, FUNCT_1:2; dom (Card (disjoin F)) = dom (disjoin F) by CARD_3:def_2; then Card F = Card (disjoin F) by A58, A32, A59, FUNCT_1:2; then card (Union (disjoin F)) c= Sum (b -powerfunc_of a) by A64, CARD_3:39; then A65: exp ((card (Union (disjoin F))),(cf a)) c= exp ((Sum (b -powerfunc_of a)),(cf a)) by CARD_2:93; exp (a,b) = card (Funcs (b,a)) by CARD_2:def_3; then exp (a,b) c= card (Funcs ((cf a),(Union (disjoin F)))) by A13, A33, A15, CARD_1:10; then A66: ( exp ((exp (a,b)),(cf a)) = exp (a,(b *` (cf a))) & exp (a,b) c= exp ((Sum (b -powerfunc_of a)),(cf a)) ) by A31, A65, CARD_2:30, XBOOLE_1:1; Sum (b -powerfunc_of a) c= exp (a,b) by Th33; then A67: exp ((Sum (b -powerfunc_of a)),(cf a)) c= exp ((exp (a,b)),(cf a)) by CARD_2:93; b *` (cf a) = b by A1, Th18; hence exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) by A67, A66, XBOOLE_0:def_10; ::_thesis: verum end; Lm5: for O being Ordinal for X being finite set st X c= O holds order_type_of (RelIncl X) is finite proof let O be Ordinal; ::_thesis: for X being finite set st X c= O holds order_type_of (RelIncl X) is finite let X be finite set ; ::_thesis: ( X c= O implies order_type_of (RelIncl X) is finite ) assume X c= O ; ::_thesis: order_type_of (RelIncl X) is finite then RelIncl X is well-ordering by WELLORD2:8; then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def_2; hence order_type_of (RelIncl X) is finite by CARD_3:105; ::_thesis: verum end; theorem Th36: :: CARD_5:36 for O being Ordinal for X being finite set st X c= O holds order_type_of (RelIncl X) = card X proof let O be Ordinal; ::_thesis: for X being finite set st X c= O holds order_type_of (RelIncl X) = card X let X be finite set ; ::_thesis: ( X c= O implies order_type_of (RelIncl X) = card X ) assume A1: X c= O ; ::_thesis: order_type_of (RelIncl X) = card X then order_type_of (RelIncl X) is finite by Lm5; then reconsider o = order_type_of (RelIncl X) as Nat ; card X = card (order_type_of (RelIncl X)) by A1, Th7; then o = card X by CARD_1:def_2; hence order_type_of (RelIncl X) = card X ; ::_thesis: verum end; theorem Th37: :: CARD_5:37 for x being set for O being Ordinal st {x} c= O holds order_type_of (RelIncl {x}) = 1 proof let x be set ; ::_thesis: for O being Ordinal st {x} c= O holds order_type_of (RelIncl {x}) = 1 let O be Ordinal; ::_thesis: ( {x} c= O implies order_type_of (RelIncl {x}) = 1 ) card {x} = 1 by CARD_2:42; hence ( {x} c= O implies order_type_of (RelIncl {x}) = 1 ) by Th36; ::_thesis: verum end; theorem :: CARD_5:38 for x being set for O being Ordinal st {x} c= O holds canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x proof let x be set ; ::_thesis: for O being Ordinal st {x} c= O holds canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x let O be Ordinal; ::_thesis: ( {x} c= O implies canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x ) set X = {x}; set R = RelIncl {x}; set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})); A1: RelIncl {0} = {[0,0]} by WELLORD2:22; assume A2: {x} c= O ; ::_thesis: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x then A3: order_type_of (RelIncl {x}) = {0} by Th37, CARD_1:49; RelIncl {x} is well-ordering by A2, WELLORD2:8; then RelIncl {x}, RelIncl (order_type_of (RelIncl {x})) are_isomorphic by WELLORD2:def_2; then A4: RelIncl (order_type_of (RelIncl {x})), RelIncl {x} are_isomorphic by WELLORD1:40; RelIncl (order_type_of (RelIncl {x})) is well-ordering by WELLORD2:8; then A5: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) is_isomorphism_of RelIncl (order_type_of (RelIncl {x})), RelIncl {x} by A4, WELLORD1:def_9; then A6: rng (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {x}) by A3, WELLORD1:def_7 .= {x} by WELLORD2:def_1 ; dom (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {0}) by A5, A3, WELLORD1:def_7 .= {0} by A1, RELAT_1:173 ; hence canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x by A3, A6, FUNCT_4:112; ::_thesis: verum end; registration let O be Ordinal; let X be Subset of O; let n be set ; cluster(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> ordinal ; coherence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal proof consider phi being Ordinal-Sequence such that A1: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and phi is increasing and dom phi = order_type_of (RelIncl X) and A2: rng phi = X by Th5; percases ( n in dom phi or not n in dom phi ) ; suppose n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal then phi . n in rng phi by FUNCT_1:def_3; hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1, A2; ::_thesis: verum end; suppose not n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; end; registration let X be natural-membered set ; let n be set ; cluster(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> natural ; coherence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural proof X c= NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT ) assume x in X ; ::_thesis: x in NAT hence x in NAT by ORDINAL1:def_12; ::_thesis: verum end; then reconsider X = X as Subset of NAT ; consider phi being Ordinal-Sequence such that A1: phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and phi is increasing and dom phi = order_type_of (RelIncl X) and A2: rng phi = X by Th5; percases ( n in dom phi or not n in dom phi ) ; supposeA3: n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural phi . n in rng phi by A3, FUNCT_1:def_3; hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural by A1, A2; ::_thesis: verum end; suppose not n in dom phi ; ::_thesis: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural hence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; end; theorem :: CARD_5:39 for F being Subset of omega holds card F c= order_type_of (RelIncl F) proof let F be Subset of omega; ::_thesis: card F c= order_type_of (RelIncl F) card F = card (order_type_of (RelIncl F)) by Th7; hence card F c= order_type_of (RelIncl F) by CARD_1:8; ::_thesis: verum end;