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 )