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∈On∧ω⊆A→A∈ran⁡ℵ↔∀x∈OnA≼x→A⊆x

Proof

Step Hyp Ref Expression
1 isinfcard ⊢ω⊆A∧card⁡A=A↔A∈ran⁡ℵ
2 1 bicomi ⊢A∈ran⁡ℵ↔ω⊆A∧card⁡A=A
3 2 baib ⊢ω⊆A→A∈ran⁡ℵ↔card⁡A=A
4 3 adantl ⊢A∈On∧ω⊆A→A∈ran⁡ℵ↔card⁡A=A
5 onenon ⊢A∈On→A∈dom⁡card
6 5 adantr ⊢A∈On∧ω⊆A→A∈dom⁡card
7 onenon ⊢x∈On→x∈dom⁡card
8 carddom2 ⊢A∈dom⁡card∧x∈dom⁡card→card⁡A⊆card⁡x↔A≼x
9 6 7 8 syl2an ⊢A∈On∧ω⊆A∧x∈On→card⁡A⊆card⁡x↔A≼x
10 cardonle ⊢x∈On→card⁡x⊆x
11 10 adantl ⊢A∈On∧ω⊆A∧x∈On→card⁡x⊆x
12 sstr ⊢card⁡A⊆card⁡x∧card⁡x⊆x→card⁡A⊆x
13 12 expcom ⊢card⁡x⊆x→card⁡A⊆card⁡x→card⁡A⊆x
14 11 13 syl ⊢A∈On∧ω⊆A∧x∈On→card⁡A⊆card⁡x→card⁡A⊆x
15 9 14 sylbird ⊢A∈On∧ω⊆A∧x∈On→A≼x→card⁡A⊆x
16 sseq1 ⊢card⁡A=A→card⁡A⊆x↔A⊆x
17 16 imbi2d ⊢card⁡A=A→A≼x→card⁡A⊆x↔A≼x→A⊆x
18 15 17 syl5ibcom ⊢A∈On∧ω⊆A∧x∈On→card⁡A=A→A≼x→A⊆x
19 18 ralrimdva ⊢A∈On∧ω⊆A→card⁡A=A→∀x∈OnA≼x→A⊆x
20 oncardid ⊢A∈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∈On→A≼card⁡A
24 23 adantr ⊢A∈On∧ω⊆A→A≼card⁡A
25 cardon ⊢card⁡A∈On
26 breq2 ⊢x=card⁡A→A≼x↔A≼card⁡A
27 sseq2 ⊢x=card⁡A→A⊆x↔A⊆card⁡A
28 26 27 imbi12d ⊢x=card⁡A→A≼x→A⊆x↔A≼card⁡A→A⊆card⁡A
29 28 rspcv ⊢card⁡A∈On→∀x∈OnA≼x→A⊆x→A≼card⁡A→A⊆card⁡A
30 25 29 ax-mp ⊢∀x∈OnA≼x→A⊆x→A≼card⁡A→A⊆card⁡A
31 24 30 syl5com ⊢A∈On∧ω⊆A→∀x∈OnA≼x→A⊆x→A⊆card⁡A
32 cardonle ⊢A∈On→card⁡A⊆A
33 32 adantr ⊢A∈On∧ω⊆A→card⁡A⊆A
34 33 biantrurd ⊢A∈On∧ω⊆A→A⊆card⁡A↔card⁡A⊆A∧A⊆card⁡A
35 eqss ⊢card⁡A=A↔card⁡A⊆A∧A⊆card⁡A
36 34 35 bitr4di ⊢A∈On∧ω⊆A→A⊆card⁡A↔card⁡A=A
37 31 36 sylibd ⊢A∈On∧ω⊆A→∀x∈OnA≼x→A⊆x→card⁡A=A
38 19 37 impbid ⊢A∈On∧ω⊆A→card⁡A=A↔∀x∈OnA≼x→A⊆x
39 4 38 bitrd ⊢A∈On∧ω⊆A→A∈ran⁡ℵ↔∀x∈OnA≼x→A⊆x