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 ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 ∈ ran ℵ ↔ ∀ 𝑥 ∈ On ( 𝐴 ≼ 𝑥 → 𝐴 ⊆ 𝑥 ) ) )

Proof

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