Metamath Proof Explorer

Theorem alephinit

Description: An infinite initial ordinal is characterized by the property of being initial - that is, it is a subset of any dominating ordinal. (Contributed by Jeff Hankins, 29-Oct-2009) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion alephinit 
|- ( ( A e. On /\ _om C_ A ) -> ( A e. ran aleph <-> A. x e. On ( A ~<_ x -> A C_ x ) ) )

Proof

Step Hyp Ref Expression
1 isinfcard 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) <-> A e. ran aleph )
2 1 bicomi 
 |-  ( A e. ran aleph <-> ( _om C_ A /\ ( card ` A ) = A ) )
3 2 baib 
 |-  ( _om C_ A -> ( A e. ran aleph <-> ( card ` A ) = A ) )
4 3 adantl 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A e. ran aleph <-> ( card ` A ) = A ) )
5 onenon 
 |-  ( A e. On -> A e. dom card )
6 5 adantr 
 |-  ( ( A e. On /\ _om C_ A ) -> A e. dom card )
7 onenon 
 |-  ( x e. On -> x e. dom card )
8 carddom2 
 |-  ( ( A e. dom card /\ x e. dom card ) -> ( ( card ` A ) C_ ( card ` x ) <-> A ~<_ x ) )
9 6 7 8 syl2an 
 |-  ( ( ( A e. On /\ _om C_ A ) /\ x e. On ) -> ( ( card ` A ) C_ ( card ` x ) <-> A ~<_ x ) )
10 cardonle 
 |-  ( x e. On -> ( card ` x ) C_ x )
11 10 adantl 
 |-  ( ( ( A e. On /\ _om C_ A ) /\ x e. On ) -> ( card ` x ) C_ x )
12 sstr 
 |-  ( ( ( card ` A ) C_ ( card ` x ) /\ ( card ` x ) C_ x ) -> ( card ` A ) C_ x )
13 12 expcom 
 |-  ( ( card ` x ) C_ x -> ( ( card ` A ) C_ ( card ` x ) -> ( card ` A ) C_ x ) )
14 11 13 syl 
 |-  ( ( ( A e. On /\ _om C_ A ) /\ x e. On ) -> ( ( card ` A ) C_ ( card ` x ) -> ( card ` A ) C_ x ) )
15 9 14 sylbird 
 |-  ( ( ( A e. On /\ _om C_ A ) /\ x e. On ) -> ( A ~<_ x -> ( card ` A ) C_ x ) )
16 sseq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) C_ x <-> A C_ x ) )
17 16 imbi2d 
 |-  ( ( card ` A ) = A -> ( ( A ~<_ x -> ( card ` A ) C_ x ) <-> ( A ~<_ x -> A C_ x ) ) )
18 15 17 syl5ibcom 
 |-  ( ( ( A e. On /\ _om C_ A ) /\ x e. On ) -> ( ( card ` A ) = A -> ( A ~<_ x -> A C_ x ) ) )
19 18 ralrimdva 
 |-  ( ( A e. On /\ _om C_ A ) -> ( ( card ` A ) = A -> A. x e. On ( A ~<_ x -> A C_ x ) ) )
20 oncardid 
 |-  ( A e. On -> ( card ` A ) ~~ A )
21 ensym 
 |-  ( ( card ` A ) ~~ A -> A ~~ ( card ` A ) )
22 endom 
 |-  ( A ~~ ( card ` A ) -> A ~<_ ( card ` A ) )
23 20 21 22 3syl 
 |-  ( A e. On -> A ~<_ ( card ` A ) )
24 23 adantr 
 |-  ( ( A e. On /\ _om C_ A ) -> A ~<_ ( card ` A ) )
25 cardon 
 |-  ( card ` A ) e. On
26 breq2 
 |-  ( x = ( card ` A ) -> ( A ~<_ x <-> A ~<_ ( card ` A ) ) )
27 sseq2 
 |-  ( x = ( card ` A ) -> ( A C_ x <-> A C_ ( card ` A ) ) )
28 26 27 imbi12d 
 |-  ( x = ( card ` A ) -> ( ( A ~<_ x -> A C_ x ) <-> ( A ~<_ ( card ` A ) -> A C_ ( card ` A ) ) ) )
29 28 rspcv 
 |-  ( ( card ` A ) e. On -> ( A. x e. On ( A ~<_ x -> A C_ x ) -> ( A ~<_ ( card ` A ) -> A C_ ( card ` A ) ) ) )
30 25 29 ax-mp 
 |-  ( A. x e. On ( A ~<_ x -> A C_ x ) -> ( A ~<_ ( card ` A ) -> A C_ ( card ` A ) ) )
31 24 30 syl5com 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A. x e. On ( A ~<_ x -> A C_ x ) -> A C_ ( card ` A ) ) )
32 cardonle 
 |-  ( A e. On -> ( card ` A ) C_ A )
33 32 adantr 
 |-  ( ( A e. On /\ _om C_ A ) -> ( card ` A ) C_ A )
34 33 biantrurd 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A C_ ( card ` A ) <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) ) )
35 eqss 
 |-  ( ( card ` A ) = A <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) )
36 34 35 bitr4di 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A C_ ( card ` A ) <-> ( card ` A ) = A ) )
37 31 36 sylibd 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A. x e. On ( A ~<_ x -> A C_ x ) -> ( card ` A ) = A ) )
38 19 37 impbid 
 |-  ( ( A e. On /\ _om C_ A ) -> ( ( card ` A ) = A <-> A. x e. On ( A ~<_ x -> A C_ x ) ) )
39 4 38 bitrd 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A e. ran aleph <-> A. x e. On ( A ~<_ x -> A C_ x ) ) )