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 ⊢ A ∈ On ∧ ∅ ∈ A → ℵ ⁡ A = ⋂ x ∈ On | ∀ y ∈ A ℵ ⁡ y ≺ x

Proof

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