:: CARD_LAR semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let S, X be set ;
let Y be Subset of S;
:: original: /\
redefine func X /\ Y -> Subset of S;
coherence
X /\ Y is Subset of S
proof end;
end;

registration
cluster infinite cardinal -> being_limit_ordinal set ;
coherence
for b1 being Ordinal st b1 is cardinal & not b1 is finite holds
b1 is being_limit_ordinal
by CARD_4:32;
end;

registration
cluster non empty being_limit_ordinal -> infinite set ;
coherence
for b1 being Ordinal st not b1 is empty & b1 is being_limit_ordinal holds
not b1 is finite
proof end;
end;

registration
cluster non limit -> being_limit_ordinal non countable set ;
coherence
for b1 being Aleph st not b1 is limit holds
not b1 is countable
proof end;
end;

registration
cluster being_limit_ordinal regular non countable set ;
existence
ex b1 being Aleph st
( b1 is regular & not b1 is countable )
proof end;
end;

definition
let A be being_limit_ordinal infinite Ordinal;
let X be set ;
pred X is_unbounded_in A means :Def1: :: CARD_LAR:def 1
( X c= A & sup X = A );
pred X is_closed_in A means :Def2: :: CARD_LAR:def 2
( X c= A & ( for B being being_limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) );
end;

:: deftheorem Def1 defines is_unbounded_in CARD_LAR:def 1 :
for A being being_limit_ordinal infinite Ordinal
for X being set holds
( X is_unbounded_in A iff ( X c= A & sup X = A ) );

:: deftheorem Def2 defines is_closed_in CARD_LAR:def 2 :
for A being being_limit_ordinal infinite Ordinal
for X being set holds
( X is_closed_in A iff ( X c= A & ( for B being being_limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) ) );

definition
let A be being_limit_ordinal infinite Ordinal;
let X be set ;
pred X is_club_in A means :Def3: :: CARD_LAR:def 3
( X is_closed_in A & X is_unbounded_in A );
end;

:: deftheorem Def3 defines is_club_in CARD_LAR:def 3 :
for A being being_limit_ordinal infinite Ordinal
for X being set holds
( X is_club_in A iff ( X is_closed_in A & X is_unbounded_in A ) );

definition
let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X is unbounded means :Def4: :: CARD_LAR:def 4
sup X = A;
attr X is closed means :Def5: :: CARD_LAR:def 5
for B being being_limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X;
end;

:: deftheorem Def4 defines unbounded CARD_LAR:def 4 :
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff sup X = A );

:: deftheorem Def5 defines closed CARD_LAR:def 5 :
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is closed iff for B being being_limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X );

notation
let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
antonym bounded X for unbounded X;
end;

theorem :: CARD_LAR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: CARD_LAR:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
proof end;

theorem Th3: :: CARD_LAR:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds X c= sup X
proof end;

theorem Th4: :: CARD_LAR:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) holds
sup X is being_limit_ordinal infinite Ordinal
proof end;

theorem Th5: :: CARD_LAR:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( not X is unbounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
proof end;

theorem Th6: :: CARD_LAR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being being_limit_ordinal infinite Ordinal
for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
proof end;

theorem Th7: :: CARD_LAR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )
proof end;

theorem Th8: :: CARD_LAR:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded holds
not X is empty
proof end;

theorem Th9: :: CARD_LAR:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
proof end;

definition
let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
let B1 be Ordinal;
assume A1: X is unbounded ;
assume A2: B1 in A ;
func LBound B1,X -> Element of X equals :Def6: :: CARD_LAR:def 6
inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;
coherence
inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X
proof end;
end;

:: deftheorem Def6 defines LBound CARD_LAR:def 6 :
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A
for B1 being Ordinal st X is unbounded & B1 in A holds
LBound B1,X = inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;

theorem Th10: :: CARD_LAR:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound B1,X in X & B1 in LBound B1,X )
proof end;

theorem Th11: :: CARD_LAR:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal holds
( [#] A is closed & [#] A is unbounded )
proof end;

definition
let A be set ;
let X be Subset of A;
let Y be set ;
:: original: \
redefine func X \ Y -> Subset of A;
coherence
X \ Y is Subset of A
proof end;
end;

theorem Th12: :: CARD_LAR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )
proof end;

theorem Th13: :: CARD_LAR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B1 being Ordinal st B1 in A holds
( A \ B1 is closed & A \ B1 is unbounded )
proof end;

definition
let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X is stationary means :Def7: :: CARD_LAR:def 7
for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty;
end;

:: deftheorem Def7 defines stationary CARD_LAR:def 7 :
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is stationary iff for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty );

theorem Th14: :: CARD_LAR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X, Y being Subset of A st X is stationary & X c= Y holds
Y is stationary
proof end;

definition
let A be being_limit_ordinal infinite Ordinal;
let X be set ;
pred X is_stationary_in A means :Def8: :: CARD_LAR:def 8
( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) );
end;

:: deftheorem Def8 defines is_stationary_in CARD_LAR:def 8 :
for A being being_limit_ordinal infinite Ordinal
for X being set holds
( X is_stationary_in A iff ( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) ) );

theorem :: CARD_LAR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds
Y is_stationary_in A
proof end;

definition
let X be set ;
let S be Subset-Family of X;
:: original: Element
redefine mode Element of S -> Subset of X;
coherence
for b1 being Element of S holds b1 is Subset of X
proof end;
end;

theorem :: CARD_LAR:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st X is stationary holds
X is unbounded
proof end;

definition
let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
func limpoints X -> Subset of A equals :: CARD_LAR:def 9
{ B1 where B1 is Element of A : ( not B1 is finite & B1 is being_limit_ordinal & sup (X /\ B1) = B1 ) } ;
coherence
{ B1 where B1 is Element of A : ( not B1 is finite & B1 is being_limit_ordinal & sup (X /\ B1) = B1 ) } is Subset of A
proof end;
end;

:: deftheorem defines limpoints CARD_LAR:def 9 :
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X = { B1 where B1 is Element of A : ( not B1 is finite & B1 is being_limit_ordinal & sup (X /\ B1) = B1 ) } ;

theorem Th17: :: CARD_LAR:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B3, B1 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
proof end;

theorem :: CARD_LAR:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
proof end;

theorem Th19: :: CARD_LAR:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X is closed
proof end;

theorem Th20: :: CARD_LAR:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded & not limpoints X is unbounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
proof end;

registration
let M be non countable Aleph;
cluster being_limit_ordinal infinite cardinal Element of M;
existence
ex b1 being Element of M st
( b1 is cardinal & not b1 is finite )
proof end;
end;

theorem Th21: :: CARD_LAR:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph
for X being Subset of M st X is unbounded holds
cf M <=` Card X
proof end;

theorem Th22: :: CARD_LAR:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph
for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds
meet S is closed
proof end;

theorem Th23: :: CARD_LAR:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M holds
for f being Function of NAT ,X holds sup (rng f) in M
proof end;

theorem :: CARD_LAR:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st alef 0 <` cf M holds
for S being non empty Subset-Family of M st Card S <` cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )
proof end;

theorem Th25: :: CARD_LAR:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M & X is unbounded holds
for B1 being Ordinal st B1 in M holds
ex B being being_limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
proof end;

theorem :: CARD_LAR:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M & X is unbounded holds
limpoints X is unbounded
proof end;

definition
let M be non countable Aleph;
attr M is Mahlo means :Def10: :: CARD_LAR:def 10
{ N where N is infinite cardinal Element of M : N is regular } is_stationary_in M;
attr M is strongly_Mahlo means :Def11: :: CARD_LAR:def 11
{ N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M;
end;

:: deftheorem Def10 defines Mahlo CARD_LAR:def 10 :
for M being non countable Aleph holds
( M is Mahlo iff { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M );

:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def 11 :
for M being non countable Aleph holds
( M is strongly_Mahlo iff { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M );

notation
let M be non countable Aleph;
synonym M is_Mahlo for Mahlo M;
synonym M is_strongly_Mahlo for strongly_Mahlo M;
end;

theorem Th27: :: CARD_LAR:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_Mahlo holds
M is Mahlo
proof end;

theorem Th28: :: CARD_LAR:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is Mahlo holds
M is regular
proof end;

theorem Th29: :: CARD_LAR:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is Mahlo holds
M is limit
proof end;

theorem :: CARD_LAR:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is Mahlo holds
M is inaccessible
proof end;

theorem Th31: :: CARD_LAR:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_Mahlo holds
M is strong_limit
proof end;

theorem :: CARD_LAR:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_Mahlo holds
M is strongly_inaccessible
proof end;

theorem Th33: :: CARD_LAR:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) holds
union X is Cardinal
proof end;

theorem Th34: :: CARD_LAR:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for M being Aleph st Card X <` cf M & ( for Y being set st Y in X holds
Card Y <` M ) holds
Card (union X) in M
proof end;

deffunc H1( Ordinal) -> set = Rank $1;

theorem Th35: :: CARD_LAR:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph
for A being Ordinal st M is strongly_inaccessible & A in M holds
Card (Rank A) <` M
proof end;

theorem Th36: :: CARD_LAR:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_inaccessible holds
Card (Rank M) = M
proof end;

theorem Th37: :: CARD_LAR:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_Tarski-Class
proof end;

theorem Th38: :: CARD_LAR:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Ordinal holds not Rank A is empty
proof end;

registration
let A be non empty Ordinal;
cluster Rank A -> non empty ;
coherence
not Rank A is empty
by Th38;
end;

theorem Th39: :: CARD_LAR:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Universe
proof end;

theorem :: CARD_LAR:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_a_model_of_ZF
proof end;