Metamath Proof Explorer

Theorem alephval3

Description: An alternate way to express the value of the aleph function: it is the least infinite cardinal different from all values at smaller arguments. Definition of aleph in Enderton p. 212 and definition of aleph in BellMachover p. 490 . (Contributed by NM, 16-Nov-2003)

Ref Expression
Assertion alephval3 ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 alephcard ⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )
2 1 a1i ⊢ ( 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
3 alephgeom ⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
4 3 biimpi ⊢ ( 𝐴 ∈ On → ω ⊆ ( ℵ ‘ 𝐴 ) )
5 alephord2i ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
6 elirr ⊢ ¬ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑦 )
7 eleq2 ⊢ ( ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) → ( ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑦 ) ) )
8 6 7 mtbiri ⊢ ( ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) → ¬ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
9 8 con2i ⊢ ( ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) → ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) )
10 5 9 syl6 ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) )
11 10 ralrimiv ⊢ ( 𝐴 ∈ On → ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) )
12 fvex ⊢ ( ℵ ‘ 𝐴 ) ∈ V
13 fveq2 ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( card ‘ 𝑥 ) = ( card ‘ ( ℵ ‘ 𝐴 ) ) )
14 id ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → 𝑥 = ( ℵ ‘ 𝐴 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) ) )
16 sseq2 ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ω ⊆ 𝑥 ↔ ω ⊆ ( ℵ ‘ 𝐴 ) ) )
17 eqeq1 ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( 𝑥 = ( ℵ ‘ 𝑦 ) ↔ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) )
18 17 notbid ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ↔ ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) )
19 18 ralbidv ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) )
20 15 16 19 3anbi123d ⊢ ( 𝑥 = ( ℵ ‘ 𝐴 ) → ( ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) ↔ ( ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) ∧ ω ⊆ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) ) )
21 12 20 elab ⊢ ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ↔ ( ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) ∧ ω ⊆ ( ℵ ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( ℵ ‘ 𝐴 ) = ( ℵ ‘ 𝑦 ) ) )
22 2 4 11 21 syl3anbrc ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } )
23 eleq1 ⊢ ( 𝑧 = ( ℵ ‘ 𝑦 ) → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
24 alephord2 ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ 𝐴 ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
25 24 bicomd ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ↔ 𝑦 ∈ 𝐴 ) )
26 23 25 sylan9bbr ⊢ ( ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) ↔ 𝑦 ∈ 𝐴 ) )
27 26 biimpcd ⊢ ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ( ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) → 𝑦 ∈ 𝐴 ) )
28 simpr ⊢ ( ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) → 𝑧 = ( ℵ ‘ 𝑦 ) )
29 27 28 jca2 ⊢ ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ( ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) )
30 29 exp4c ⊢ ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( 𝑧 = ( ℵ ‘ 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) ) ) )
31 30 com3r ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ( 𝑦 ∈ On → ( 𝑧 = ( ℵ ‘ 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) ) ) )
32 31 imp4b ⊢ ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) → ( ( 𝑦 ∈ On ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) )
33 32 reximdv2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) → ( ∃ 𝑦 ∈ On 𝑧 = ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑧 = ( ℵ ‘ 𝑦 ) ) )
34 cardalephex ⊢ ( ω ⊆ 𝑧 → ( ( card ‘ 𝑧 ) = 𝑧 ↔ ∃ 𝑦 ∈ On 𝑧 = ( ℵ ‘ 𝑦 ) ) )
35 34 biimpac ⊢ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) → ∃ 𝑦 ∈ On 𝑧 = ( ℵ ‘ 𝑦 ) )
36 33 35 impel ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) ∧ ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐴 𝑧 = ( ℵ ‘ 𝑦 ) )
37 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 = ( ℵ ‘ 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) )
38 36 37 sylib ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) ∧ ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ) → ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) )
39 nan ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) → ¬ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) ↔ ( ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) ∧ ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ) → ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
40 38 39 mpbir ⊢ ( ( 𝐴 ∈ On ∧ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ) → ¬ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
41 40 ex ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ¬ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) )
42 vex ⊢ 𝑧 ∈ V
43 fveq2 ⊢ ( 𝑥 = 𝑧 → ( card ‘ 𝑥 ) = ( card ‘ 𝑧 ) )
44 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
45 43 44 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ 𝑧 ) = 𝑧 ) )
46 sseq2 ⊢ ( 𝑥 = 𝑧 → ( ω ⊆ 𝑥 ↔ ω ⊆ 𝑧 ) )
47 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( ℵ ‘ 𝑦 ) ↔ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
48 47 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ↔ ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
49 48 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
50 45 46 49 3anbi123d ⊢ ( 𝑥 = 𝑧 → ( ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) ↔ ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) ) )
51 42 50 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ↔ ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
52 df-3an ⊢ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) ↔ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
53 51 52 bitri ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ↔ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
54 53 notbii ⊢ ( ¬ 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ↔ ¬ ( ( ( card ‘ 𝑧 ) = 𝑧 ∧ ω ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑧 = ( ℵ ‘ 𝑦 ) ) )
55 41 54 syl6ibr ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ ( ℵ ‘ 𝐴 ) → ¬ 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ) )
56 55 ralrimiv ⊢ ( 𝐴 ∈ On → ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } )
57 cardon ⊢ ( card ‘ 𝑥 ) ∈ On
58 eleq1 ⊢ ( ( card ‘ 𝑥 ) = 𝑥 → ( ( card ‘ 𝑥 ) ∈ On ↔ 𝑥 ∈ On ) )
59 57 58 mpbii ⊢ ( ( card ‘ 𝑥 ) = 𝑥 → 𝑥 ∈ On )
60 59 3ad2ant1 ⊢ ( ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) → 𝑥 ∈ On )
61 60 abssi ⊢ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ⊆ On
62 oneqmini ⊢ ( { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ⊆ On → ( ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ) )
63 61 62 ax-mp ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ∧ ∀ 𝑧 ∈ ( ℵ ‘ 𝐴 ) ¬ 𝑧 ∈ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } ) → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } )
64 22 56 63 syl2anc ⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( ( card ‘ 𝑥 ) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 = ( ℵ ‘ 𝑦 ) ) } )