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∈Oncard⁡z=ℵ⁡x
24 22 23 mpbii ⊢ω⊆card⁡z→∃x∈Oncard⁡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∈Oncard⁡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 biimtrid ⊢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 imbitrdi ⊢∅∈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