This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 alephordi 
 |-  ( A e. On -> ( y e. A -> ( aleph ` y ) ~< ( aleph ` A ) ) )
2 1 ralrimiv 
 |-  ( A e. On -> A. y e. A ( aleph ` y ) ~< ( aleph ` A ) )
3 alephon 
 |-  ( aleph ` A ) e. On
4 2 3 jctil 
 |-  ( A e. On -> ( ( aleph ` A ) e. On /\ A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
5 breq2 
 |-  ( x = ( aleph ` A ) -> ( ( aleph ` y ) ~< x <-> ( aleph ` y ) ~< ( aleph ` A ) ) )
6 5 ralbidv 
 |-  ( x = ( aleph ` A ) -> ( A. y e. A ( aleph ` y ) ~< x <-> A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
7 6 elrab 
 |-  ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } <-> ( ( aleph ` A ) e. On /\ A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
8 4 7 sylibr 
 |-  ( A e. On -> ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
9 cardsdomelir 
 |-  ( z e. ( card ` ( aleph ` A ) ) -> z ~< ( aleph ` A ) )
10 alephcard 
 |-  ( card ` ( aleph ` A ) ) = ( aleph ` A )
11 10 eqcomi 
 |-  ( aleph ` A ) = ( card ` ( aleph ` A ) )
12 9 11 eleq2s 
 |-  ( z e. ( aleph ` A ) -> z ~< ( aleph ` A ) )
13 omex 
 |-  _om e. _V
14 vex 
 |-  z e. _V
15 entri3 
 |-  ( ( _om e. _V /\ z e. _V ) -> ( _om ~<_ z \/ z ~<_ _om ) )
16 13 14 15 mp2an 
 |-  ( _om ~<_ z \/ z ~<_ _om )
17 carddom 
 |-  ( ( _om e. _V /\ z e. _V ) -> ( ( card ` _om ) C_ ( card ` z ) <-> _om ~<_ z ) )
18 13 14 17 mp2an 
 |-  ( ( card ` _om ) C_ ( card ` z ) <-> _om ~<_ z )
19 cardom 
 |-  ( card ` _om ) = _om
20 19 sseq1i 
 |-  ( ( card ` _om ) C_ ( card ` z ) <-> _om C_ ( card ` z ) )
21 18 20 bitr3i 
 |-  ( _om ~<_ z <-> _om C_ ( card ` z ) )
22 cardidm 
 |-  ( card ` ( card ` z ) ) = ( card ` z )
23 cardalephex 
 |-  ( _om C_ ( card ` z ) -> ( ( card ` ( card ` z ) ) = ( card ` z ) <-> E. x e. On ( card ` z ) = ( aleph ` x ) ) )
24 22 23 mpbii 
 |-  ( _om C_ ( card ` z ) -> E. x e. On ( card ` z ) = ( aleph ` x ) )
25 alephord 
 |-  ( ( x e. On /\ A e. On ) -> ( x e. A <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
26 25 ancoms 
 |-  ( ( A e. On /\ x e. On ) -> ( x e. A <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
27 breq1 
 |-  ( ( card ` z ) = ( aleph ` x ) -> ( ( card ` z ) ~< ( aleph ` A ) <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
28 14 cardid 
 |-  ( card ` z ) ~~ z
29 sdomen1 
 |-  ( ( card ` z ) ~~ z -> ( ( card ` z ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) ) )
30 28 29 ax-mp 
 |-  ( ( card ` z ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) )
31 27 30 bitr3di 
 |-  ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) ) )
32 26 31 sylan9bb 
 |-  ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( x e. A <-> z ~< ( aleph ` A ) ) )
33 fveq2 
 |-  ( y = x -> ( aleph ` y ) = ( aleph ` x ) )
34 33 breq1d 
 |-  ( y = x -> ( ( aleph ` y ) ~< z <-> ( aleph ` x ) ~< z ) )
35 34 rspcv 
 |-  ( x e. A -> ( A. y e. A ( aleph ` y ) ~< z -> ( aleph ` x ) ~< z ) )
36 sdomirr 
 |-  -. ( aleph ` x ) ~< ( aleph ` x )
37 sdomen2 
 |-  ( ( card ` z ) ~~ z -> ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< z ) )
38 28 37 ax-mp 
 |-  ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< z )
39 breq2 
 |-  ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< ( aleph ` x ) ) )
40 38 39 bitr3id 
 |-  ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< z <-> ( aleph ` x ) ~< ( aleph ` x ) ) )
41 36 40 mtbiri 
 |-  ( ( card ` z ) = ( aleph ` x ) -> -. ( aleph ` x ) ~< z )
42 35 41 nsyli 
 |-  ( x e. A -> ( ( card ` z ) = ( aleph ` x ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
43 42 com12 
 |-  ( ( card ` z ) = ( aleph ` x ) -> ( x e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
44 43 adantl 
 |-  ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( x e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
45 32 44 sylbird 
 |-  ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
46 45 rexlimdva2 
 |-  ( A e. On -> ( E. x e. On ( card ` z ) = ( aleph ` x ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
47 24 46 syl5 
 |-  ( A e. On -> ( _om C_ ( card ` z ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
48 21 47 biimtrid 
 |-  ( A e. On -> ( _om ~<_ z -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
49 48 adantr 
 |-  ( ( A e. On /\ (/) e. A ) -> ( _om ~<_ z -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
50 ne0i 
 |-  ( (/) e. A -> A =/= (/) )
51 onelon 
 |-  ( ( A e. On /\ y e. A ) -> y e. On )
52 alephgeom 
 |-  ( y e. On <-> _om C_ ( aleph ` y ) )
53 alephon 
 |-  ( aleph ` y ) e. On
54 ssdomg 
 |-  ( ( aleph ` y ) e. On -> ( _om C_ ( aleph ` y ) -> _om ~<_ ( aleph ` y ) ) )
55 53 54 ax-mp 
 |-  ( _om C_ ( aleph ` y ) -> _om ~<_ ( aleph ` y ) )
56 52 55 sylbi 
 |-  ( y e. On -> _om ~<_ ( aleph ` y ) )
57 domtr 
 |-  ( ( z ~<_ _om /\ _om ~<_ ( aleph ` y ) ) -> z ~<_ ( aleph ` y ) )
58 56 57 sylan2 
 |-  ( ( z ~<_ _om /\ y e. On ) -> z ~<_ ( aleph ` y ) )
59 domnsym 
 |-  ( z ~<_ ( aleph ` y ) -> -. ( aleph ` y ) ~< z )
60 58 59 syl 
 |-  ( ( z ~<_ _om /\ y e. On ) -> -. ( aleph ` y ) ~< z )
61 51 60 sylan2 
 |-  ( ( z ~<_ _om /\ ( A e. On /\ y e. A ) ) -> -. ( aleph ` y ) ~< z )
62 61 expr 
 |-  ( ( z ~<_ _om /\ A e. On ) -> ( y e. A -> -. ( aleph ` y ) ~< z ) )
63 62 ralrimiv 
 |-  ( ( z ~<_ _om /\ A e. On ) -> A. y e. A -. ( aleph ` y ) ~< z )
64 r19.2z 
 |-  ( ( A =/= (/) /\ A. y e. A -. ( aleph ` y ) ~< z ) -> E. y e. A -. ( aleph ` y ) ~< z )
65 64 ex 
 |-  ( A =/= (/) -> ( A. y e. A -. ( aleph ` y ) ~< z -> E. y e. A -. ( aleph ` y ) ~< z ) )
66 50 63 65 syl2im 
 |-  ( (/) e. A -> ( ( z ~<_ _om /\ A e. On ) -> E. y e. A -. ( aleph ` y ) ~< z ) )
67 rexnal 
 |-  ( E. y e. A -. ( aleph ` y ) ~< z <-> -. A. y e. A ( aleph ` y ) ~< z )
68 66 67 imbitrdi 
 |-  ( (/) e. A -> ( ( z ~<_ _om /\ A e. On ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
69 68 com12 
 |-  ( ( z ~<_ _om /\ A e. On ) -> ( (/) e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
70 69 expimpd 
 |-  ( z ~<_ _om -> ( ( A e. On /\ (/) e. A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
71 70 a1d 
 |-  ( z ~<_ _om -> ( z ~< ( aleph ` A ) -> ( ( A e. On /\ (/) e. A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
72 71 com3r 
 |-  ( ( A e. On /\ (/) e. A ) -> ( z ~<_ _om -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
73 49 72 jaod 
 |-  ( ( A e. On /\ (/) e. A ) -> ( ( _om ~<_ z \/ z ~<_ _om ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
74 16 73 mpi 
 |-  ( ( A e. On /\ (/) e. A ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
75 breq2 
 |-  ( x = z -> ( ( aleph ` y ) ~< x <-> ( aleph ` y ) ~< z ) )
76 75 ralbidv 
 |-  ( x = z -> ( A. y e. A ( aleph ` y ) ~< x <-> A. y e. A ( aleph ` y ) ~< z ) )
77 76 elrab 
 |-  ( z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } <-> ( z e. On /\ A. y e. A ( aleph ` y ) ~< z ) )
78 77 simprbi 
 |-  ( z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } -> A. y e. A ( aleph ` y ) ~< z )
79 78 con3i 
 |-  ( -. A. y e. A ( aleph ` y ) ~< z -> -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
80 12 74 79 syl56 
 |-  ( ( A e. On /\ (/) e. A ) -> ( z e. ( aleph ` A ) -> -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) )
81 80 ralrimiv 
 |-  ( ( A e. On /\ (/) e. A ) -> A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
82 ssrab2 
 |-  { x e. On | A. y e. A ( aleph ` y ) ~< x } C_ On
83 oneqmini 
 |-  ( { x e. On | A. y e. A ( aleph ` y ) ~< x } C_ On -> ( ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } /\ A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } ) )
84 82 83 ax-mp 
 |-  ( ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } /\ A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } )
85 8 81 84 syl2an2r 
 |-  ( ( A e. On /\ (/) e. A ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } )