Metamath Proof Explorer

Theorem alephordi

Description: Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephordi ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅ ) )
2 fveq2 ⊢ ( 𝑥 = ∅ → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ ∅ ) )
3 2 breq2d ⊢ ( 𝑥 = ∅ → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ ∅ ) ) )
4 1 3 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ∅ → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ ∅ ) ) ) )
5 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
6 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) )
7 6 breq2d ⊢ ( 𝑥 = 𝑦 → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) )
8 5 7 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) ) )
9 eleq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦 ) )
10 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ suc 𝑦 ) )
11 10 breq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
13 eleq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
14 fveq2 ⊢ ( 𝑥 = 𝐵 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐵 ) )
15 14 breq2d ⊢ ( 𝑥 = 𝐵 → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) ) )
17 noel ⊢ ¬ 𝐴 ∈ ∅
18 17 pm2.21i ⊢ ( 𝐴 ∈ ∅ → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ ∅ ) )
19 vex ⊢ 𝑦 ∈ V
20 19 elsuc2 ⊢ ( 𝐴 ∈ suc 𝑦 ↔ ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) )
21 alephordilem1 ⊢ ( 𝑦 ∈ On → ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ suc 𝑦 ) )
22 sdomtr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ suc 𝑦 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) )
23 21 22 sylan2 ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ∧ 𝑦 ∈ On ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) )
24 23 expcom ⊢ ( 𝑦 ∈ On → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) )
25 24 imim2d ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
26 25 com23 ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ 𝑦 → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
27 fveq2 ⊢ ( 𝐴 = 𝑦 → ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) )
28 27 breq1d ⊢ ( 𝐴 = 𝑦 → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ suc 𝑦 ) ) )
29 21 28 imbitrrid ⊢ ( 𝐴 = 𝑦 → ( 𝑦 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) )
30 29 a1d ⊢ ( 𝐴 = 𝑦 → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( 𝑦 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
31 30 com3r ⊢ ( 𝑦 ∈ On → ( 𝐴 = 𝑦 → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
32 26 31 jaod ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
33 20 32 biimtrid ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ suc 𝑦 → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
34 33 com23 ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝑦 ) ) ) )
35 fvexd ⊢ ( Lim 𝑥 → ( ℵ ‘ 𝑥 ) ∈ V )
36 fveq2 ⊢ ( 𝑤 = 𝐴 → ( ℵ ‘ 𝑤 ) = ( ℵ ‘ 𝐴 ) )
37 36 ssiun2s ⊢ ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ⊆ ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) )
38 vex ⊢ 𝑥 ∈ V
39 alephlim ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( ℵ ‘ 𝑥 ) = ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) )
40 38 39 mpan ⊢ ( Lim 𝑥 → ( ℵ ‘ 𝑥 ) = ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) )
41 40 sseq2d ⊢ ( Lim 𝑥 → ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝐴 ) ⊆ ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) ) )
42 37 41 imbitrrid ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) ) )
43 ssdomg ⊢ ( ( ℵ ‘ 𝑥 ) ∈ V → ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ) )
44 35 42 43 sylsyld ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ) )
45 limsuc ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
46 fveq2 ⊢ ( 𝑤 = suc 𝐴 → ( ℵ ‘ 𝑤 ) = ( ℵ ‘ suc 𝐴 ) )
47 46 ssiun2s ⊢ ( suc 𝐴 ∈ 𝑥 → ( ℵ ‘ suc 𝐴 ) ⊆ ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) )
48 40 sseq2d ⊢ ( Lim 𝑥 → ( ( ℵ ‘ suc 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ suc 𝐴 ) ⊆ ∪ 𝑤 ∈ 𝑥 ( ℵ ‘ 𝑤 ) ) )
49 47 48 imbitrrid ⊢ ( Lim 𝑥 → ( suc 𝐴 ∈ 𝑥 → ( ℵ ‘ suc 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) ) )
50 ssdomg ⊢ ( ( ℵ ‘ 𝑥 ) ∈ V → ( ( ℵ ‘ suc 𝐴 ) ⊆ ( ℵ ‘ 𝑥 ) → ( ℵ ‘ suc 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ) )
51 35 49 50 sylsyld ⊢ ( Lim 𝑥 → ( suc 𝐴 ∈ 𝑥 → ( ℵ ‘ suc 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ) )
52 45 51 sylbid ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ( ℵ ‘ suc 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ) )
53 52 imp ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( ℵ ‘ suc 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) )
54 domnsym ⊢ ( ( ℵ ‘ suc 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) → ¬ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) )
55 53 54 syl ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ¬ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) )
56 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
57 38 56 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
58 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ 𝑥 ) → 𝐴 ∈ On )
59 57 58 sylan ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → 𝐴 ∈ On )
60 ensym ⊢ ( ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) → ( ℵ ‘ 𝑥 ) ≈ ( ℵ ‘ 𝐴 ) )
61 alephordilem1 ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) )
62 ensdomtr ⊢ ( ( ( ℵ ‘ 𝑥 ) ≈ ( ℵ ‘ 𝐴 ) ∧ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) )
63 62 ex ⊢ ( ( ℵ ‘ 𝑥 ) ≈ ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) → ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) ) )
64 60 61 63 syl2im ⊢ ( ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) → ( 𝐴 ∈ On → ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) ) )
65 59 64 syl5com ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ( ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) → ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ suc 𝐴 ) ) )
66 55 65 mtod ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) → ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) )
67 66 ex ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) ) )
68 44 67 jcad ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ∧ ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) ) ) )
69 brsdom ⊢ ( ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ↔ ( ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝑥 ) ∧ ¬ ( ℵ ‘ 𝐴 ) ≈ ( ℵ ‘ 𝑥 ) ) )
70 68 69 imbitrrdi ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) )
71 70 a1d ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∈ 𝑦 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑦 ) ) → ( 𝐴 ∈ 𝑥 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝑥 ) ) ) )
72 4 8 12 16 18 34 71 tfinds ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ 𝐵 ) ) )