Metamath Proof Explorer

Theorem alephval2

Description: An alternate way to express the value of the aleph function for nonzero arguments. Theorem 64 of Suppes p. 229. (Contributed by NM, 15-Nov-2003)

Ref Expression
Assertion alephval2 ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )

Proof

Step Hyp Ref Expression
1 alephordi ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) ) )
2 1 ralrimiv ⊢ ( 𝐴 ∈ On → ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) )
3 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
4 2 3 jctil ⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) ) )
5 breq2 ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝑦 ) ≺ 𝑥 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) ) )
6 5 ralbidv ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) ) )
7 6 elrab ⊢ ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ↔ ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝐴 ) ) )
8 4 7 sylibr ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )
9 cardsdomelir ⊢ ( 𝑧 ∈ ( card ‘ ( ℵ ‘ 𝐴 ) ) → 𝑧 ≺ ( ℵ ‘ 𝐴 ) )
10 alephcard ⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )
11 10 eqcomi ⊢ ( ℵ ‘ 𝐴 ) = ( card ‘ ( ℵ ‘ 𝐴 ) )
12 9 11 eleq2s ⊢ ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → 𝑧 ≺ ( ℵ ‘ 𝐴 ) )
13 omex ⊢ ω ∈ V
14 vex ⊢ 𝑧 ∈ V
15 entri3 ⊢ ( ( ω ∈ V ∧ 𝑧 ∈ V ) → ( ω ≼ 𝑧 ∨ 𝑧 ≼ ω ) )
16 13 14 15 mp2an ⊢ ( ω ≼ 𝑧 ∨ 𝑧 ≼ ω )
17 carddom ⊢ ( ( ω ∈ V ∧ 𝑧 ∈ V ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝑧 ) ↔ ω ≼ 𝑧 ) )
18 13 14 17 mp2an ⊢ ( ( card ‘ ω ) ⊆ ( card ‘ 𝑧 ) ↔ ω ≼ 𝑧 )
19 cardom ⊢ ( card ‘ ω ) = ω
20 19 sseq1i ⊢ ( ( card ‘ ω ) ⊆ ( card ‘ 𝑧 ) ↔ ω ⊆ ( card ‘ 𝑧 ) )
21 18 20 bitr3i ⊢ ( ω ≼ 𝑧 ↔ ω ⊆ ( card ‘ 𝑧 ) )
22 cardidm ⊢ ( card ‘ ( card ‘ 𝑧 ) ) = ( card ‘ 𝑧 )
23 cardalephex ⊢ ( ω ⊆ ( card ‘ 𝑧 ) → ( ( card ‘ ( card ‘ 𝑧 ) ) = ( card ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ On ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) ) )
24 22 23 mpbii ⊢ ( ω ⊆ ( card ‘ 𝑧 ) → ∃ 𝑥 ∈ On ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) )
25 alephord ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑥 ∈ 𝐴 ↔ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝐴 ) ) )
26 25 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑥 ∈ 𝐴 ↔ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝐴 ) ) )
27 breq1 ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( ( card ‘ 𝑧 ) ≺ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝐴 ) ) )
28 14 cardid ⊢ ( card ‘ 𝑧 ) ≈ 𝑧
29 sdomen1 ⊢ ( ( card ‘ 𝑧 ) ≈ 𝑧 → ( ( card ‘ 𝑧 ) ≺ ( ℵ ‘ 𝐴 ) ↔ 𝑧 ≺ ( ℵ ‘ 𝐴 ) ) )
30 28 29 ax-mp ⊢ ( ( card ‘ 𝑧 ) ≺ ( ℵ ‘ 𝐴 ) ↔ 𝑧 ≺ ( ℵ ‘ 𝐴 ) )
31 27 30 bitr3di ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝐴 ) ↔ 𝑧 ≺ ( ℵ ‘ 𝐴 ) ) )
32 26 31 sylan9bb ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ≺ ( ℵ ‘ 𝐴 ) ) )
33 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑥 ) )
34 33 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( ℵ ‘ 𝑦 ) ≺ 𝑧 ↔ ( ℵ ‘ 𝑥 ) ≺ 𝑧 ) )
35 34 rspcv ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 → ( ℵ ‘ 𝑥 ) ≺ 𝑧 ) )
36 sdomirr ⊢ ¬ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑥 )
37 sdomen2 ⊢ ( ( card ‘ 𝑧 ) ≈ 𝑧 → ( ( ℵ ‘ 𝑥 ) ≺ ( card ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑥 ) ≺ 𝑧 ) )
38 28 37 ax-mp ⊢ ( ( ℵ ‘ 𝑥 ) ≺ ( card ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑥 ) ≺ 𝑧 )
39 breq2 ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( ( ℵ ‘ 𝑥 ) ≺ ( card ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑥 ) ) )
40 38 39 bitr3id ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( ( ℵ ‘ 𝑥 ) ≺ 𝑧 ↔ ( ℵ ‘ 𝑥 ) ≺ ( ℵ ‘ 𝑥 ) ) )
41 36 40 mtbiri ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ¬ ( ℵ ‘ 𝑥 ) ≺ 𝑧 )
42 35 41 nsyli ⊢ ( 𝑥 ∈ 𝐴 → ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
43 42 com12 ⊢ ( ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( 𝑥 ∈ 𝐴 → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
44 43 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
45 32 44 sylbird ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) ) → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
46 45 rexlimdva2 ⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ On ( card ‘ 𝑧 ) = ( ℵ ‘ 𝑥 ) → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
47 24 46 syl5 ⊢ ( 𝐴 ∈ On → ( ω ⊆ ( card ‘ 𝑧 ) → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
48 21 47 syl5bi ⊢ ( 𝐴 ∈ On → ( ω ≼ 𝑧 → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
49 48 adantr ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ω ≼ 𝑧 → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
50 ne0i ⊢ ( ∅ ∈ 𝐴 → 𝐴 ≠ ∅ )
51 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
52 alephgeom ⊢ ( 𝑦 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝑦 ) )
53 alephon ⊢ ( ℵ ‘ 𝑦 ) ∈ On
54 ssdomg ⊢ ( ( ℵ ‘ 𝑦 ) ∈ On → ( ω ⊆ ( ℵ ‘ 𝑦 ) → ω ≼ ( ℵ ‘ 𝑦 ) ) )
55 53 54 ax-mp ⊢ ( ω ⊆ ( ℵ ‘ 𝑦 ) → ω ≼ ( ℵ ‘ 𝑦 ) )
56 52 55 sylbi ⊢ ( 𝑦 ∈ On → ω ≼ ( ℵ ‘ 𝑦 ) )
57 domtr ⊢ ( ( 𝑧 ≼ ω ∧ ω ≼ ( ℵ ‘ 𝑦 ) ) → 𝑧 ≼ ( ℵ ‘ 𝑦 ) )
58 56 57 sylan2 ⊢ ( ( 𝑧 ≼ ω ∧ 𝑦 ∈ On ) → 𝑧 ≼ ( ℵ ‘ 𝑦 ) )
59 domnsym ⊢ ( 𝑧 ≼ ( ℵ ‘ 𝑦 ) → ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
60 58 59 syl ⊢ ( ( 𝑧 ≼ ω ∧ 𝑦 ∈ On ) → ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
61 51 60 sylan2 ⊢ ( ( 𝑧 ≼ ω ∧ ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
62 61 expr ⊢ ( ( 𝑧 ≼ ω ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 → ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
63 62 ralrimiv ⊢ ( ( 𝑧 ≼ ω ∧ 𝐴 ∈ On ) → ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
64 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) → ∃ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
65 64 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 → ∃ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
66 50 63 65 syl2im ⊢ ( ∅ ∈ 𝐴 → ( ( 𝑧 ≼ ω ∧ 𝐴 ∈ On ) → ∃ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
67 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
68 66 67 syl6ib ⊢ ( ∅ ∈ 𝐴 → ( ( 𝑧 ≼ ω ∧ 𝐴 ∈ On ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
69 68 com12 ⊢ ( ( 𝑧 ≼ ω ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
70 69 expimpd ⊢ ( 𝑧 ≼ ω → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
71 70 a1d ⊢ ( 𝑧 ≼ ω → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
72 71 com3r ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ≼ ω → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
73 49 72 jaod ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ( ω ≼ 𝑧 ∨ 𝑧 ≼ ω ) → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) ) )
74 16 73 mpi ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ≺ ( ℵ ‘ 𝐴 ) → ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
75 breq2 ⊢ ( 𝑥 = 𝑧 → ( ( ℵ ‘ 𝑦 ) ≺ 𝑥 ↔ ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
76 75 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
77 76 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ↔ ( 𝑧 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 ) )
78 77 simprbi ⊢ ( 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } → ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 )
79 78 con3i ⊢ ( ¬ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑧 → ¬ 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )
80 12 74 79 syl56 ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ¬ 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ) )
81 80 ralrimiv ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )
82 ssrab2 ⊢ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ⊆ On
83 oneqmini ⊢ ( { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ⊆ On → ( ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ) )
84 82 83 ax-mp ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )
85 8 81 84 syl2an2r ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ≺ 𝑥 } )