Theorem r1sdom 8242

Description: Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)

Assertion

Ref	Expression
r1sdom	|- ( ( A e. On /\ B e. A ) -> ( R1 ` B ) ~< ( R1 ` A ) )

Proof of Theorem r1sdom

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

Step	Hyp	Ref	Expression
1		eleq2 2517	. . . 4 |- ( x = (/) -> ( B e. x <-> B e. (/) ) )
2		fveq2 5863	. . . . 5 |- ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
3	2	breq2d 4413	. . . 4 |- ( x = (/) -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` (/) ) ) )
4	1, 3	imbi12d 322	. . 3 |- ( x = (/) -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. (/) -> ( R1 ` B ) ~< ( R1 ` (/) ) ) ) )
5		eleq2 2517	. . . 4 |- ( x = y -> ( B e. x <-> B e. y ) )
6		fveq2 5863	. . . . 5 |- ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
7	6	breq2d 4413	. . . 4 |- ( x = y -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` y ) ) )
8	5, 7	imbi12d 322	. . 3 |- ( x = y -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) ) )
9		eleq2 2517	. . . 4 |- ( x = suc y -> ( B e. x <-> B e. suc y ) )
10		fveq2 5863	. . . . 5 |- ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
11	10	breq2d 4413	. . . 4 |- ( x = suc y -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
12	9, 11	imbi12d 322	. . 3 |- ( x = suc y -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. suc y -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
13		eleq2 2517	. . . 4 |- ( x = A -> ( B e. x <-> B e. A ) )
14		fveq2 5863	. . . . 5 |- ( x = A -> ( R1 ` x ) = ( R1 ` A ) )
15	14	breq2d 4413	. . . 4 |- ( x = A -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` A ) ) )
16	13, 15	imbi12d 322	. . 3 |- ( x = A -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. A -> ( R1 ` B ) ~< ( R1 ` A ) ) ) )
17		noel 3734	. . . 4 |- -. B e. (/)
18	17	pm2.21i 135	. . 3 |- ( B e. (/) -> ( R1 ` B ) ~< ( R1 ` (/) ) )
19		elsuci 5488	. . . . 5 |- ( B e. suc y -> ( B e. y \/ B = y ) )
20		fvex 5873	. . . . . . . . . . 11 |- ( R1 ` y ) e. _V
21	20	canth2 7722	. . . . . . . . . 10 |- ( R1 ` y ) ~< ~P ( R1 ` y )
22		r1suc 8238	. . . . . . . . . 10 |- ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
23	21, 22	syl5breqr 4438	. . . . . . . . 9 |- ( y e. On -> ( R1 ` y ) ~< ( R1 ` suc y ) )
24		sdomtr 7707	. . . . . . . . . 10 |- ( ( ( R1 ` B ) ~< ( R1 ` y ) /\ ( R1 ` y ) ~< ( R1 ` suc y ) ) -> ( R1 ` B ) ~< ( R1 ` suc y ) )
25	24	expcom 437	. . . . . . . . 9 |- ( ( R1 ` y ) ~< ( R1 ` suc y ) -> ( ( R1 ` B ) ~< ( R1 ` y ) -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
26	23, 25	syl 17	. . . . . . . 8 |- ( y e. On -> ( ( R1 ` B ) ~< ( R1 ` y ) -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
27	26	com12 32	. . . . . . 7 |- ( ( R1 ` B ) ~< ( R1 ` y ) -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
28	27	imim2i 16	. . . . . 6 |- ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
29		fveq2 5863	. . . . . . . . 9 |- ( B = y -> ( R1 ` B ) = ( R1 ` y ) )
30	29	breq1d 4411	. . . . . . . 8 |- ( B = y -> ( ( R1 ` B ) ~< ( R1 ` suc y ) <-> ( R1 ` y ) ~< ( R1 ` suc y ) ) )
31	23, 30	syl5ibr 225	. . . . . . 7 |- ( B = y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
32	31	a1i 11	. . . . . 6 |- ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B = y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
33	28, 32	jaod 382	. . . . 5 |- ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( ( B e. y \/ B = y ) -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
34	19, 33	syl5 33	. . . 4 |- ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. suc y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
35	34	com3r 82	. . 3 |- ( y e. On -> ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. suc y -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
36		limuni 5482	. . . . . . 7 |- ( Lim x -> x = U. x )
37	36	eleq2d 2513	. . . . . 6 |- ( Lim x -> ( B e. x <-> B e. U. x ) )
38		eluni2 4201	. . . . . 6 |- ( B e. U. x <-> E. y e. x B e. y )
39	37, 38	syl6bb 265	. . . . 5 |- ( Lim x -> ( B e. x <-> E. y e. x B e. y ) )
40		r19.29 2924	. . . . . . 7 |- ( ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ E. y e. x B e. y ) -> E. y e. x ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) )
41		fvex 5873	. . . . . . . . . . 11 |- ( R1 ` x ) e. _V
42	41	a1i 11	. . . . . . . . . 10 |- ( Lim x -> ( R1 ` x ) e. _V )
43		ssiun2 4320	. . . . . . . . . . 11 |- ( y e. x -> ( R1 ` y ) C_ U_ y e. x ( R1 ` y ) )
44		vex 3047	. . . . . . . . . . . . 13 |- x e. _V
45		r1lim 8240	. . . . . . . . . . . . 13 |- ( ( x e. _V /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
46	44, 45	mpan 675	. . . . . . . . . . . 12 |- ( Lim x -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
47	46	sseq2d 3459	. . . . . . . . . . 11 |- ( Lim x -> ( ( R1 ` y ) C_ ( R1 ` x ) <-> ( R1 ` y ) C_ U_ y e. x ( R1 ` y ) ) )
48	43, 47	syl5ibr 225	. . . . . . . . . 10 |- ( Lim x -> ( y e. x -> ( R1 ` y ) C_ ( R1 ` x ) ) )
49		ssdomg 7612	. . . . . . . . . 10 |- ( ( R1 ` x ) e. _V -> ( ( R1 ` y ) C_ ( R1 ` x ) -> ( R1 ` y ) ~<_ ( R1 ` x ) ) )
50	42, 48, 49	sylsyld 58	. . . . . . . . 9 |- ( Lim x -> ( y e. x -> ( R1 ` y ) ~<_ ( R1 ` x ) ) )
51		id 22	. . . . . . . . . . 11 |- ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) )
52	51	imp 431	. . . . . . . . . 10 |- ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` y ) )
53		sdomdomtr 7702	. . . . . . . . . . 11 |- ( ( ( R1 ` B ) ~< ( R1 ` y ) /\ ( R1 ` y ) ~<_ ( R1 ` x ) ) -> ( R1 ` B ) ~< ( R1 ` x ) )
54	53	expcom 437	. . . . . . . . . 10 |- ( ( R1 ` y ) ~<_ ( R1 ` x ) -> ( ( R1 ` B ) ~< ( R1 ` y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
55	52, 54	syl5 33	. . . . . . . . 9 |- ( ( R1 ` y ) ~<_ ( R1 ` x ) -> ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
56	50, 55	syl6 34	. . . . . . . 8 |- ( Lim x -> ( y e. x -> ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
57	56	rexlimdv 2876	. . . . . . 7 |- ( Lim x -> ( E. y e. x ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
58	40, 57	syl5 33	. . . . . 6 |- ( Lim x -> ( ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ E. y e. x B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
59	58	expcomd 440	. . . . 5 |- ( Lim x -> ( E. y e. x B e. y -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
60	39, 59	sylbid 219	. . . 4 |- ( Lim x -> ( B e. x -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
61	60	com23 81	. . 3 |- ( Lim x -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
62	4, 8, 12, 16, 18, 35, 61	tfinds 6683	. 2 |- ( A e. On -> ( B e. A -> ( R1 ` B ) ~< ( R1 ` A ) ) )
63	62	imp 431	1 |- ( ( A e. On /\ B e. A ) -> ( R1 ` B ) ~< ( R1 ` A ) )

Syntax hints:   -> wi 4   \/ wo 370   /\ wa 371   = wceq 1443   e. wcel 1886   A.wral 2736   E.wrex 2737   _Vcvv 3044   C_ wss 3403   (/)c0 3730   ~Pcpw 3950   U.cuni 4197   U_ciun 4277   class class class wbr 4401   Oncon0 5422   Lim wlim 5423   suc csuc 5424   ` cfv 5581   ~<_ cdom 7564   ~< csdm 7565   R1cr1 8230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-r1 8232

This theorem is referenced by:  r111  8243  smobeth  9008  r1tskina  9204