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