Metamath Proof Explorer

Theorem smobeth

Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather beth_A is the same as ( card( R1( _om +o A ) ) ) , since conventionally we start counting at the first infinite level, and ignore the finite levels. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 2-Jun-2015)

Ref Expression
Assertion smobeth 
|- Smo ( card o. R1 )

Proof

Step Hyp Ref Expression
1 cardf2 
 |-  card : { x | E. y e. On y ~~ x } --> On
2 ffun 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> Fun card )
3 1 2 ax-mp 
 |-  Fun card
4 r1fnon 
 |-  R1 Fn On
5 fnfun 
 |-  ( R1 Fn On -> Fun R1 )
6 4 5 ax-mp 
 |-  Fun R1
7 funco 
 |-  ( ( Fun card /\ Fun R1 ) -> Fun ( card o. R1 ) )
8 3 6 7 mp2an 
 |-  Fun ( card o. R1 )
9 funfn 
 |-  ( Fun ( card o. R1 ) <-> ( card o. R1 ) Fn dom ( card o. R1 ) )
10 8 9 mpbi 
 |-  ( card o. R1 ) Fn dom ( card o. R1 )
11 rnco 
 |-  ran ( card o. R1 ) = ran ( card |` ran R1 )
12 resss 
 |-  ( card |` ran R1 ) C_ card
13 12 rnssi 
 |-  ran ( card |` ran R1 ) C_ ran card
14 frn 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> ran card C_ On )
15 1 14 ax-mp 
 |-  ran card C_ On
16 13 15 sstri 
 |-  ran ( card |` ran R1 ) C_ On
17 11 16 eqsstri 
 |-  ran ( card o. R1 ) C_ On
18 df-f 
 |-  ( ( card o. R1 ) : dom ( card o. R1 ) --> On <-> ( ( card o. R1 ) Fn dom ( card o. R1 ) /\ ran ( card o. R1 ) C_ On ) )
19 10 17 18 mpbir2an 
 |-  ( card o. R1 ) : dom ( card o. R1 ) --> On
20 dmco 
 |-  dom ( card o. R1 ) = ( `' R1 " dom card )
21 20 feq2i 
 |-  ( ( card o. R1 ) : dom ( card o. R1 ) --> On <-> ( card o. R1 ) : ( `' R1 " dom card ) --> On )
22 19 21 mpbi 
 |-  ( card o. R1 ) : ( `' R1 " dom card ) --> On
23 elpreima 
 |-  ( R1 Fn On -> ( x e. ( `' R1 " dom card ) <-> ( x e. On /\ ( R1 ` x ) e. dom card ) ) )
24 4 23 ax-mp 
 |-  ( x e. ( `' R1 " dom card ) <-> ( x e. On /\ ( R1 ` x ) e. dom card ) )
25 24 simplbi 
 |-  ( x e. ( `' R1 " dom card ) -> x e. On )
26 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
27 25 26 sylan 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> y e. On )
28 24 simprbi 
 |-  ( x e. ( `' R1 " dom card ) -> ( R1 ` x ) e. dom card )
29 28 adantr 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` x ) e. dom card )
30 r1ord2 
 |-  ( x e. On -> ( y e. x -> ( R1 ` y ) C_ ( R1 ` x ) ) )
31 30 imp 
 |-  ( ( x e. On /\ y e. x ) -> ( R1 ` y ) C_ ( R1 ` x ) )
32 25 31 sylan 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) C_ ( R1 ` x ) )
33 ssnum 
 |-  ( ( ( R1 ` x ) e. dom card /\ ( R1 ` y ) C_ ( R1 ` x ) ) -> ( R1 ` y ) e. dom card )
34 29 32 33 syl2anc 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) e. dom card )
35 elpreima 
 |-  ( R1 Fn On -> ( y e. ( `' R1 " dom card ) <-> ( y e. On /\ ( R1 ` y ) e. dom card ) ) )
36 4 35 ax-mp 
 |-  ( y e. ( `' R1 " dom card ) <-> ( y e. On /\ ( R1 ` y ) e. dom card ) )
37 27 34 36 sylanbrc 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> y e. ( `' R1 " dom card ) )
38 37 rgen2 
 |-  A. x e. ( `' R1 " dom card ) A. y e. x y e. ( `' R1 " dom card )
39 dftr5 
 |-  ( Tr ( `' R1 " dom card ) <-> A. x e. ( `' R1 " dom card ) A. y e. x y e. ( `' R1 " dom card ) )
40 38 39 mpbir 
 |-  Tr ( `' R1 " dom card )
41 cnvimass 
 |-  ( `' R1 " dom card ) C_ dom R1
42 dffn2 
 |-  ( R1 Fn On <-> R1 : On --> _V )
43 4 42 mpbi 
 |-  R1 : On --> _V
44 43 fdmi 
 |-  dom R1 = On
45 41 44 sseqtri 
 |-  ( `' R1 " dom card ) C_ On
46 epweon 
 |-  _E We On
47 wess 
 |-  ( ( `' R1 " dom card ) C_ On -> ( _E We On -> _E We ( `' R1 " dom card ) ) )
48 45 46 47 mp2 
 |-  _E We ( `' R1 " dom card )
49 df-ord 
 |-  ( Ord ( `' R1 " dom card ) <-> ( Tr ( `' R1 " dom card ) /\ _E We ( `' R1 " dom card ) ) )
50 40 48 49 mpbir2an 
 |-  Ord ( `' R1 " dom card )
51 r1sdom 
 |-  ( ( x e. On /\ y e. x ) -> ( R1 ` y ) ~< ( R1 ` x ) )
52 25 51 sylan 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) ~< ( R1 ` x ) )
53 cardsdom2 
 |-  ( ( ( R1 ` y ) e. dom card /\ ( R1 ` x ) e. dom card ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) <-> ( R1 ` y ) ~< ( R1 ` x ) ) )
54 34 29 53 syl2anc 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) <-> ( R1 ` y ) ~< ( R1 ` x ) ) )
55 52 54 mpbird 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) )
56 fvco2 
 |-  ( ( R1 Fn On /\ y e. On ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
57 4 27 56 sylancr 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
58 25 adantr 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> x e. On )
59 fvco2 
 |-  ( ( R1 Fn On /\ x e. On ) -> ( ( card o. R1 ) ` x ) = ( card ` ( R1 ` x ) ) )
60 4 58 59 sylancr 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` x ) = ( card ` ( R1 ` x ) ) )
61 55 57 60 3eltr4d 
 |-  ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) )
62 61 ex 
 |-  ( x e. ( `' R1 " dom card ) -> ( y e. x -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) ) )
63 62 adantl 
 |-  ( ( y e. ( `' R1 " dom card ) /\ x e. ( `' R1 " dom card ) ) -> ( y e. x -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) ) )
64 22 50 63 20 issmo 
 |-  Smo ( card o. R1 )