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 
|- ( A e. On -> ( aleph ` A ) = |^| { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } )

Proof

Step Hyp Ref Expression
1 alephcard 
 |-  ( card ` ( aleph ` A ) ) = ( aleph ` A )
2 1 a1i 
 |-  ( A e. On -> ( card ` ( aleph ` A ) ) = ( aleph ` A ) )
3 alephgeom 
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
4 3 biimpi 
 |-  ( A e. On -> _om C_ ( aleph ` A ) )
5 alephord2i 
 |-  ( A e. On -> ( y e. A -> ( aleph ` y ) e. ( aleph ` A ) ) )
6 elirr 
 |-  -. ( aleph ` y ) e. ( aleph ` y )
7 eleq2 
 |-  ( ( aleph ` A ) = ( aleph ` y ) -> ( ( aleph ` y ) e. ( aleph ` A ) <-> ( aleph ` y ) e. ( aleph ` y ) ) )
8 6 7 mtbiri 
 |-  ( ( aleph ` A ) = ( aleph ` y ) -> -. ( aleph ` y ) e. ( aleph ` A ) )
9 8 con2i 
 |-  ( ( aleph ` y ) e. ( aleph ` A ) -> -. ( aleph ` A ) = ( aleph ` y ) )
10 5 9 syl6 
 |-  ( A e. On -> ( y e. A -> -. ( aleph ` A ) = ( aleph ` y ) ) )
11 10 ralrimiv 
 |-  ( A e. On -> A. y e. A -. ( aleph ` A ) = ( aleph ` y ) )
12 fvex 
 |-  ( aleph ` A ) e. _V
13 fveq2 
 |-  ( x = ( aleph ` A ) -> ( card ` x ) = ( card ` ( aleph ` A ) ) )
14 id 
 |-  ( x = ( aleph ` A ) -> x = ( aleph ` A ) )
15 13 14 eqeq12d 
 |-  ( x = ( aleph ` A ) -> ( ( card ` x ) = x <-> ( card ` ( aleph ` A ) ) = ( aleph ` A ) ) )
16 sseq2 
 |-  ( x = ( aleph ` A ) -> ( _om C_ x <-> _om C_ ( aleph ` A ) ) )
17 eqeq1 
 |-  ( x = ( aleph ` A ) -> ( x = ( aleph ` y ) <-> ( aleph ` A ) = ( aleph ` y ) ) )
18 17 notbid 
 |-  ( x = ( aleph ` A ) -> ( -. x = ( aleph ` y ) <-> -. ( aleph ` A ) = ( aleph ` y ) ) )
19 18 ralbidv 
 |-  ( x = ( aleph ` A ) -> ( A. y e. A -. x = ( aleph ` y ) <-> A. y e. A -. ( aleph ` A ) = ( aleph ` y ) ) )
20 15 16 19 3anbi123d 
 |-  ( x = ( aleph ` A ) -> ( ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) <-> ( ( card ` ( aleph ` A ) ) = ( aleph ` A ) /\ _om C_ ( aleph ` A ) /\ A. y e. A -. ( aleph ` A ) = ( aleph ` y ) ) ) )
21 12 20 elab 
 |-  ( ( aleph ` A ) e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } <-> ( ( card ` ( aleph ` A ) ) = ( aleph ` A ) /\ _om C_ ( aleph ` A ) /\ A. y e. A -. ( aleph ` A ) = ( aleph ` y ) ) )
22 2 4 11 21 syl3anbrc 
 |-  ( A e. On -> ( aleph ` A ) e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } )
23 eleq1 
 |-  ( z = ( aleph ` y ) -> ( z e. ( aleph ` A ) <-> ( aleph ` y ) e. ( aleph ` A ) ) )
24 alephord2 
 |-  ( ( y e. On /\ A e. On ) -> ( y e. A <-> ( aleph ` y ) e. ( aleph ` A ) ) )
25 24 bicomd 
 |-  ( ( y e. On /\ A e. On ) -> ( ( aleph ` y ) e. ( aleph ` A ) <-> y e. A ) )
26 23 25 sylan9bbr 
 |-  ( ( ( y e. On /\ A e. On ) /\ z = ( aleph ` y ) ) -> ( z e. ( aleph ` A ) <-> y e. A ) )
27 26 biimpcd 
 |-  ( z e. ( aleph ` A ) -> ( ( ( y e. On /\ A e. On ) /\ z = ( aleph ` y ) ) -> y e. A ) )
28 simpr 
 |-  ( ( ( y e. On /\ A e. On ) /\ z = ( aleph ` y ) ) -> z = ( aleph ` y ) )
29 27 28 jca2 
 |-  ( z e. ( aleph ` A ) -> ( ( ( y e. On /\ A e. On ) /\ z = ( aleph ` y ) ) -> ( y e. A /\ z = ( aleph ` y ) ) ) )
30 29 exp4c 
 |-  ( z e. ( aleph ` A ) -> ( y e. On -> ( A e. On -> ( z = ( aleph ` y ) -> ( y e. A /\ z = ( aleph ` y ) ) ) ) ) )
31 30 com3r 
 |-  ( A e. On -> ( z e. ( aleph ` A ) -> ( y e. On -> ( z = ( aleph ` y ) -> ( y e. A /\ z = ( aleph ` y ) ) ) ) ) )
32 31 imp4b 
 |-  ( ( A e. On /\ z e. ( aleph ` A ) ) -> ( ( y e. On /\ z = ( aleph ` y ) ) -> ( y e. A /\ z = ( aleph ` y ) ) ) )
33 32 reximdv2 
 |-  ( ( A e. On /\ z e. ( aleph ` A ) ) -> ( E. y e. On z = ( aleph ` y ) -> E. y e. A z = ( aleph ` y ) ) )
34 cardalephex 
 |-  ( _om C_ z -> ( ( card ` z ) = z <-> E. y e. On z = ( aleph ` y ) ) )
35 34 biimpac 
 |-  ( ( ( card ` z ) = z /\ _om C_ z ) -> E. y e. On z = ( aleph ` y ) )
36 33 35 impel 
 |-  ( ( ( A e. On /\ z e. ( aleph ` A ) ) /\ ( ( card ` z ) = z /\ _om C_ z ) ) -> E. y e. A z = ( aleph ` y ) )
37 dfrex2 
 |-  ( E. y e. A z = ( aleph ` y ) <-> -. A. y e. A -. z = ( aleph ` y ) )
38 36 37 sylib 
 |-  ( ( ( A e. On /\ z e. ( aleph ` A ) ) /\ ( ( card ` z ) = z /\ _om C_ z ) ) -> -. A. y e. A -. z = ( aleph ` y ) )
39 nan 
 |-  ( ( ( A e. On /\ z e. ( aleph ` A ) ) -> -. ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) ) <-> ( ( ( A e. On /\ z e. ( aleph ` A ) ) /\ ( ( card ` z ) = z /\ _om C_ z ) ) -> -. A. y e. A -. z = ( aleph ` y ) ) )
40 38 39 mpbir 
 |-  ( ( A e. On /\ z e. ( aleph ` A ) ) -> -. ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) )
41 40 ex 
 |-  ( A e. On -> ( z e. ( aleph ` A ) -> -. ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) ) )
42 vex 
 |-  z e. _V
43 fveq2 
 |-  ( x = z -> ( card ` x ) = ( card ` z ) )
44 id 
 |-  ( x = z -> x = z )
45 43 44 eqeq12d 
 |-  ( x = z -> ( ( card ` x ) = x <-> ( card ` z ) = z ) )
46 sseq2 
 |-  ( x = z -> ( _om C_ x <-> _om C_ z ) )
47 eqeq1 
 |-  ( x = z -> ( x = ( aleph ` y ) <-> z = ( aleph ` y ) ) )
48 47 notbid 
 |-  ( x = z -> ( -. x = ( aleph ` y ) <-> -. z = ( aleph ` y ) ) )
49 48 ralbidv 
 |-  ( x = z -> ( A. y e. A -. x = ( aleph ` y ) <-> A. y e. A -. z = ( aleph ` y ) ) )
50 45 46 49 3anbi123d 
 |-  ( x = z -> ( ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) <-> ( ( card ` z ) = z /\ _om C_ z /\ A. y e. A -. z = ( aleph ` y ) ) ) )
51 42 50 elab 
 |-  ( z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } <-> ( ( card ` z ) = z /\ _om C_ z /\ A. y e. A -. z = ( aleph ` y ) ) )
52 df-3an 
 |-  ( ( ( card ` z ) = z /\ _om C_ z /\ A. y e. A -. z = ( aleph ` y ) ) <-> ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) )
53 51 52 bitri 
 |-  ( z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } <-> ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) )
54 53 notbii 
 |-  ( -. z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } <-> -. ( ( ( card ` z ) = z /\ _om C_ z ) /\ A. y e. A -. z = ( aleph ` y ) ) )
55 41 54 syl6ibr 
 |-  ( A e. On -> ( z e. ( aleph ` A ) -> -. z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } ) )
56 55 ralrimiv 
 |-  ( A e. On -> A. z e. ( aleph ` A ) -. z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } )
57 cardon 
 |-  ( card ` x ) e. On
58 eleq1 
 |-  ( ( card ` x ) = x -> ( ( card ` x ) e. On <-> x e. On ) )
59 57 58 mpbii 
 |-  ( ( card ` x ) = x -> x e. On )
60 59 3ad2ant1 
 |-  ( ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) -> x e. On )
61 60 abssi 
 |-  { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } C_ On
62 oneqmini 
 |-  ( { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } C_ On -> ( ( ( aleph ` A ) e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } /\ A. z e. ( aleph ` A ) -. z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } ) -> ( aleph ` A ) = |^| { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } ) )
63 61 62 ax-mp 
 |-  ( ( ( aleph ` A ) e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } /\ A. z e. ( aleph ` A ) -. z e. { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } ) -> ( aleph ` A ) = |^| { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } )
64 22 56 63 syl2anc 
 |-  ( A e. On -> ( aleph ` A ) = |^| { x | ( ( card ` x ) = x /\ _om C_ x /\ A. y e. A -. x = ( aleph ` y ) ) } )