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