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 ∈ On A ≼ 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 ∈ On A ≼ 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 ∈ On A ≼ x → A ⊆ x → A ≼ card ⁡ A → A ⊆ card ⁡ A
30 25 29 ax-mp ⊢ ∀ x ∈ On A ≼ x → A ⊆ x → A ≼ card ⁡ A → A ⊆ card ⁡ A
31 24 30 syl5com ⊢ A ∈ On ∧ ω ⊆ A → ∀ x ∈ On A ≼ 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 ∈ On A ≼ x → A ⊆ x → card ⁡ A = A
38 19 37 impbid ⊢ A ∈ On ∧ ω ⊆ A → card ⁡ A = A ↔ ∀ x ∈ On A ≼ x → A ⊆ x
39 4 38 bitrd ⊢ A ∈ On ∧ ω ⊆ A → A ∈ ran ⁡ ℵ ↔ ∀ x ∈ On A ≼ x → A ⊆ x