Theorem smobeth 8421

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.)

Assertion

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

Proof of Theorem smobeth

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cardf2 7790	. . . . . . 7 |- card : { x | E. y e. On y ~~ x } --> On
2		ffun 5556	. . . . . . 7 |- ( card : { x | E. y e. On y ~~ x } --> On -> Fun card )
3	1, 2	ax-mp 8	. . . . . 6 |- Fun card
4		r1fnon 7653	. . . . . . 7 |- R1 Fn On
5		fnfun 5505	. . . . . . 7 |- ( R1 Fn On -> Fun R1 )
6	4, 5	ax-mp 8	. . . . . 6 |- Fun R1
7		funco 5454	. . . . . 6 |- ( ( Fun card /\ Fun R1 ) -> Fun ( card o. R1 ) )
8	3, 6, 7	mp2an 654	. . . . 5 |- Fun ( card o. R1 )
9		funfn 5445	. . . . 5 |- ( Fun ( card o. R1 ) <-> ( card o. R1 ) Fn dom ( card o. R1 ) )
10	8, 9	mpbi 200	. . . 4 |- ( card o. R1 ) Fn dom ( card o. R1 )
11		rnco 5339	. . . . 5 |- ran ( card o. R1 ) = ran ( card |` ran R1 )
12		resss 5133	. . . . . . 7 |- ( card |` ran R1 ) C_ card
13		rnss 5061	. . . . . . 7 |- ( ( card |` ran R1 ) C_ card -> ran ( card |` ran R1 ) C_ ran card )
14	12, 13	ax-mp 8	. . . . . 6 |- ran ( card |` ran R1 ) C_ ran card
15		frn 5560	. . . . . . 7 |- ( card : { x | E. y e. On y ~~ x } --> On -> ran card C_ On )
16	1, 15	ax-mp 8	. . . . . 6 |- ran card C_ On
17	14, 16	sstri 3321	. . . . 5 |- ran ( card |` ran R1 ) C_ On
18	11, 17	eqsstri 3342	. . . 4 |- ran ( card o. R1 ) C_ On
19		df-f 5421	. . . 4 |- ( ( card o. R1 ) : dom ( card o. R1 ) --> On <-> ( ( card o. R1 ) Fn dom ( card o. R1 ) /\ ran ( card o. R1 ) C_ On ) )
20	10, 18, 19	mpbir2an 887	. . 3 |- ( card o. R1 ) : dom ( card o. R1 ) --> On
21		dmco 5341	. . . 4 |- dom ( card o. R1 ) = ( `' R1 " dom card )
22	21	feq2i 5549	. . 3 |- ( ( card o. R1 ) : dom ( card o. R1 ) --> On <-> ( card o. R1 ) : ( `' R1 " dom card ) --> On )
23	20, 22	mpbi 200	. 2 |- ( card o. R1 ) : ( `' R1 " dom card ) --> On
24		elpreima 5813	. . . . . . . . 9 |- ( R1 Fn On -> ( x e. ( `' R1 " dom card ) <-> ( x e. On /\ ( R1 ` x ) e. dom card ) ) )
25	4, 24	ax-mp 8	. . . . . . . 8 |- ( x e. ( `' R1 " dom card ) <-> ( x e. On /\ ( R1 ` x ) e. dom card ) )
26	25	simplbi 447	. . . . . . 7 |- ( x e. ( `' R1 " dom card ) -> x e. On )
27		onelon 4570	. . . . . . 7 |- ( ( x e. On /\ y e. x ) -> y e. On )
28	26, 27	sylan 458	. . . . . 6 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> y e. On )
29	25	simprbi 451	. . . . . . . 8 |- ( x e. ( `' R1 " dom card ) -> ( R1 ` x ) e. dom card )
30	29	adantr 452	. . . . . . 7 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` x ) e. dom card )
31		r1ord2 7667	. . . . . . . . 9 |- ( x e. On -> ( y e. x -> ( R1 ` y ) C_ ( R1 ` x ) ) )
32	31	imp 419	. . . . . . . 8 |- ( ( x e. On /\ y e. x ) -> ( R1 ` y ) C_ ( R1 ` x ) )
33	26, 32	sylan 458	. . . . . . 7 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) C_ ( R1 ` x ) )
34		ssnum 7880	. . . . . . 7 |- ( ( ( R1 ` x ) e. dom card /\ ( R1 ` y ) C_ ( R1 ` x ) ) -> ( R1 ` y ) e. dom card )
35	30, 33, 34	syl2anc 643	. . . . . 6 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) e. dom card )
36		elpreima 5813	. . . . . . 7 |- ( R1 Fn On -> ( y e. ( `' R1 " dom card ) <-> ( y e. On /\ ( R1 ` y ) e. dom card ) ) )
37	4, 36	ax-mp 8	. . . . . 6 |- ( y e. ( `' R1 " dom card ) <-> ( y e. On /\ ( R1 ` y ) e. dom card ) )
38	28, 35, 37	sylanbrc 646	. . . . 5 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> y e. ( `' R1 " dom card ) )
39	38	rgen2 2766	. . . 4 |- A. x e. ( `' R1 " dom card ) A. y e. x y e. ( `' R1 " dom card )
40		dftr5 4269	. . . 4 |- ( Tr ( `' R1 " dom card ) <-> A. x e. ( `' R1 " dom card ) A. y e. x y e. ( `' R1 " dom card ) )
41	39, 40	mpbir 201	. . 3 |- Tr ( `' R1 " dom card )
42		cnvimass 5187	. . . . 5 |- ( `' R1 " dom card ) C_ dom R1
43		dffn2 5555	. . . . . . 7 |- ( R1 Fn On <-> R1 : On --> _V )
44	4, 43	mpbi 200	. . . . . 6 |- R1 : On --> _V
45	44	fdmi 5559	. . . . 5 |- dom R1 = On
46	42, 45	sseqtri 3344	. . . 4 |- ( `' R1 " dom card ) C_ On
47		epweon 4727	. . . 4 |- _E We On
48		wess 4533	. . . 4 |- ( ( `' R1 " dom card ) C_ On -> ( _E We On -> _E We ( `' R1 " dom card ) ) )
49	46, 47, 48	mp2 9	. . 3 |- _E We ( `' R1 " dom card )
50		df-ord 4548	. . 3 |- ( Ord ( `' R1 " dom card ) <-> ( Tr ( `' R1 " dom card ) /\ _E We ( `' R1 " dom card ) ) )
51	41, 49, 50	mpbir2an 887	. 2 |- Ord ( `' R1 " dom card )
52		r1sdom 7660	. . . . . . 7 |- ( ( x e. On /\ y e. x ) -> ( R1 ` y ) ~< ( R1 ` x ) )
53	26, 52	sylan 458	. . . . . 6 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( R1 ` y ) ~< ( R1 ` x ) )
54		cardsdom2 7835	. . . . . . 7 |- ( ( ( R1 ` y ) e. dom card /\ ( R1 ` x ) e. dom card ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) <-> ( R1 ` y ) ~< ( R1 ` x ) ) )
55	35, 30, 54	syl2anc 643	. . . . . 6 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) <-> ( R1 ` y ) ~< ( R1 ` x ) ) )
56	53, 55	mpbird 224	. . . . 5 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( card ` ( R1 ` y ) ) e. ( card ` ( R1 ` x ) ) )
57		fvco2 5761	. . . . . 6 |- ( ( R1 Fn On /\ y e. On ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
58	4, 28, 57	sylancr 645	. . . . 5 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
59	26	adantr 452	. . . . . 6 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> x e. On )
60		fvco2 5761	. . . . . 6 |- ( ( R1 Fn On /\ x e. On ) -> ( ( card o. R1 ) ` x ) = ( card ` ( R1 ` x ) ) )
61	4, 59, 60	sylancr 645	. . . . 5 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` x ) = ( card ` ( R1 ` x ) ) )
62	56, 58, 61	3eltr4d 2489	. . . 4 |- ( ( x e. ( `' R1 " dom card ) /\ y e. x ) -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) )
63	62	ex 424	. . 3 |- ( x e. ( `' R1 " dom card ) -> ( y e. x -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) ) )
64	63	adantl 453	. 2 |- ( ( y e. ( `' R1 " dom card ) /\ x e. ( `' R1 " dom card ) ) -> ( y e. x -> ( ( card o. R1 ) ` y ) e. ( ( card o. R1 ) ` x ) ) )
65	23, 51, 64, 21	issmo 6573	1 |- Smo ( card o. R1 )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   {cab 2394   A.wral 2670   E.wrex 2671   _Vcvv 2920   C_ wss 3284   class class class wbr 4176   Tr wtr 4266   _E cep 4456   We wwe 4504   Ord word 4544   Oncon0 4545   `'ccnv 4840   dom cdm 4841   ran crn 4842   |` cres 4843   "cima 4844   o. ccom 4845   Fun wfun 5411   Fn wfn 5412   -->wf 5413   ` cfv 5417   Smo wsmo 6570   ~~ cen 7069   ~< csdm 7071   R1cr1 7648   cardccrd 7782

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rmo 2678  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-se 4506  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-riota 6512  df-smo 6571  df-recs 6596  df-rdg 6631  df-er 6868  df-en 7073  df-dom 7074  df-sdom 7075  df-r1 7650  df-card 7786