Theorem r1pwss 7674

Description: Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)

Assertion

Ref	Expression
r1pwss	|- ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )

Proof of Theorem r1pwss

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

Step	Hyp	Ref	Expression
1		r1funlim 7656	. . . . . . 7 |- ( Fun R1 /\ Lim dom R1 )
2	1	simpri 449	. . . . . 6 |- Lim dom R1
3		limord 4608	. . . . . 6 |- ( Lim dom R1 -> Ord dom R1 )
4	2, 3	ax-mp 8	. . . . 5 |- Ord dom R1
5		ordsson 4737	. . . . 5 |- ( Ord dom R1 -> dom R1 C_ On )
6	4, 5	ax-mp 8	. . . 4 |- dom R1 C_ On
7		elfvdm 5724	. . . 4 |- ( A e. ( R1 ` B ) -> B e. dom R1 )
8	6, 7	sseldi 3314	. . 3 |- ( A e. ( R1 ` B ) -> B e. On )
9		onzsl 4793	. . 3 |- ( B e. On <-> ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) )
10	8, 9	sylib 189	. 2 |- ( A e. ( R1 ` B ) -> ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) )
11		noel 3600	. . . . 5 |- -. A e. (/)
12		fveq2 5695	. . . . . . . 8 |- ( B = (/) -> ( R1 ` B ) = ( R1 ` (/) ) )
13		r10 7658	. . . . . . . 8 |- ( R1 ` (/) ) = (/)
14	12, 13	syl6eq 2460	. . . . . . 7 |- ( B = (/) -> ( R1 ` B ) = (/) )
15	14	eleq2d 2479	. . . . . 6 |- ( B = (/) -> ( A e. ( R1 ` B ) <-> A e. (/) ) )
16	15	biimpcd 216	. . . . 5 |- ( A e. ( R1 ` B ) -> ( B = (/) -> A e. (/) ) )
17	11, 16	mtoi 171	. . . 4 |- ( A e. ( R1 ` B ) -> -. B = (/) )
18	17	pm2.21d 100	. . 3 |- ( A e. ( R1 ` B ) -> ( B = (/) -> ~P A C_ ( R1 ` B ) ) )
19		simpl 444	. . . . . . . 8 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> A e. ( R1 ` B ) )
20		simpr 448	. . . . . . . . . 10 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> B = suc x )
21	20	fveq2d 5699	. . . . . . . . 9 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` B ) = ( R1 ` suc x ) )
22	7	adantr 452	. . . . . . . . . . . 12 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> B e. dom R1 )
23	20, 22	eqeltrrd 2487	. . . . . . . . . . 11 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> suc x e. dom R1 )
24		limsuc 4796	. . . . . . . . . . . 12 |- ( Lim dom R1 -> ( x e. dom R1 <-> suc x e. dom R1 ) )
25	2, 24	ax-mp 8	. . . . . . . . . . 11 |- ( x e. dom R1 <-> suc x e. dom R1 )
26	23, 25	sylibr 204	. . . . . . . . . 10 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> x e. dom R1 )
27		r1sucg 7659	. . . . . . . . . 10 |- ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
28	26, 27	syl 16	. . . . . . . . 9 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
29	21, 28	eqtrd 2444	. . . . . . . 8 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` B ) = ~P ( R1 ` x ) )
30	19, 29	eleqtrd 2488	. . . . . . 7 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> A e. ~P ( R1 ` x ) )
31		elpwi 3775	. . . . . . . 8 |- ( A e. ~P ( R1 ` x ) -> A C_ ( R1 ` x ) )
32		sspwb 4381	. . . . . . . 8 |- ( A C_ ( R1 ` x ) <-> ~P A C_ ~P ( R1 ` x ) )
33	31, 32	sylib 189	. . . . . . 7 |- ( A e. ~P ( R1 ` x ) -> ~P A C_ ~P ( R1 ` x ) )
34	30, 33	syl 16	. . . . . 6 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ~P A C_ ~P ( R1 ` x ) )
35	34, 29	sseqtr4d 3353	. . . . 5 |- ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ~P A C_ ( R1 ` B ) )
36	35	ex 424	. . . 4 |- ( A e. ( R1 ` B ) -> ( B = suc x -> ~P A C_ ( R1 ` B ) ) )
37	36	rexlimdvw 2801	. . 3 |- ( A e. ( R1 ` B ) -> ( E. x e. On B = suc x -> ~P A C_ ( R1 ` B ) ) )
38		r1tr 7666	. . . . . 6 |- Tr ( R1 ` B )
39		simpl 444	. . . . . . . . . . 11 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> A e. ( R1 ` B ) )
40		r1limg 7661	. . . . . . . . . . . 12 |- ( ( B e. dom R1 /\ Lim B ) -> ( R1 ` B ) = U_ x e. B ( R1 ` x ) )
41	7, 40	sylan 458	. . . . . . . . . . 11 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> ( R1 ` B ) = U_ x e. B ( R1 ` x ) )
42	39, 41	eleqtrd 2488	. . . . . . . . . 10 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> A e. U_ x e. B ( R1 ` x ) )
43		eliun 4065	. . . . . . . . . 10 |- ( A e. U_ x e. B ( R1 ` x ) <-> E. x e. B A e. ( R1 ` x ) )
44	42, 43	sylib 189	. . . . . . . . 9 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> E. x e. B A e. ( R1 ` x ) )
45		simprl 733	. . . . . . . . . . . 12 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> x e. B )
46		limsuc 4796	. . . . . . . . . . . . 13 |- ( Lim B -> ( x e. B <-> suc x e. B ) )
47	46	ad2antlr 708	. . . . . . . . . . . 12 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( x e. B <-> suc x e. B ) )
48	45, 47	mpbid 202	. . . . . . . . . . 11 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc x e. B )
49		limsuc 4796	. . . . . . . . . . . 12 |- ( Lim B -> ( suc x e. B <-> suc suc x e. B ) )
50	49	ad2antlr 708	. . . . . . . . . . 11 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( suc x e. B <-> suc suc x e. B ) )
51	48, 50	mpbid 202	. . . . . . . . . 10 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc suc x e. B )
52		r1tr 7666	. . . . . . . . . . . . . . 15 |- Tr ( R1 ` x )
53		simprr 734	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> A e. ( R1 ` x ) )
54		trss 4279	. . . . . . . . . . . . . . 15 |- ( Tr ( R1 ` x ) -> ( A e. ( R1 ` x ) -> A C_ ( R1 ` x ) ) )
55	52, 53, 54	mpsyl 61	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> A C_ ( R1 ` x ) )
56	55, 32	sylib 189	. . . . . . . . . . . . 13 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A C_ ~P ( R1 ` x ) )
57	7	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> B e. dom R1 )
58		ordtr1 4592	. . . . . . . . . . . . . . . 16 |- ( Ord dom R1 -> ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 ) )
59	4, 58	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 )
60	45, 57, 59	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> x e. dom R1 )
61	60, 27	syl 16	. . . . . . . . . . . . 13 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
62	56, 61	sseqtr4d 3353	. . . . . . . . . . . 12 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A C_ ( R1 ` suc x ) )
63		fvex 5709	. . . . . . . . . . . . 13 |- ( R1 ` suc x ) e. _V
64	63	elpw2 4332	. . . . . . . . . . . 12 |- ( ~P A e. ~P ( R1 ` suc x ) <-> ~P A C_ ( R1 ` suc x ) )
65	62, 64	sylibr 204	. . . . . . . . . . 11 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A e. ~P ( R1 ` suc x ) )
66	60, 25	sylib 189	. . . . . . . . . . . 12 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc x e. dom R1 )
67		r1sucg 7659	. . . . . . . . . . . 12 |- ( suc x e. dom R1 -> ( R1 ` suc suc x ) = ~P ( R1 ` suc x ) )
68	66, 67	syl 16	. . . . . . . . . . 11 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( R1 ` suc suc x ) = ~P ( R1 ` suc x ) )
69	65, 68	eleqtrrd 2489	. . . . . . . . . 10 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A e. ( R1 ` suc suc x ) )
70		fveq2 5695	. . . . . . . . . . . 12 |- ( y = suc suc x -> ( R1 ` y ) = ( R1 ` suc suc x ) )
71	70	eleq2d 2479	. . . . . . . . . . 11 |- ( y = suc suc x -> ( ~P A e. ( R1 ` y ) <-> ~P A e. ( R1 ` suc suc x ) ) )
72	71	rspcev 3020	. . . . . . . . . 10 |- ( ( suc suc x e. B /\ ~P A e. ( R1 ` suc suc x ) ) -> E. y e. B ~P A e. ( R1 ` y ) )
73	51, 69, 72	syl2anc 643	. . . . . . . . 9 |- ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> E. y e. B ~P A e. ( R1 ` y ) )
74	44, 73	rexlimddv 2802	. . . . . . . 8 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> E. y e. B ~P A e. ( R1 ` y ) )
75		eliun 4065	. . . . . . . 8 |- ( ~P A e. U_ y e. B ( R1 ` y ) <-> E. y e. B ~P A e. ( R1 ` y ) )
76	74, 75	sylibr 204	. . . . . . 7 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A e. U_ y e. B ( R1 ` y ) )
77		r1limg 7661	. . . . . . . 8 |- ( ( B e. dom R1 /\ Lim B ) -> ( R1 ` B ) = U_ y e. B ( R1 ` y ) )
78	7, 77	sylan 458	. . . . . . 7 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> ( R1 ` B ) = U_ y e. B ( R1 ` y ) )
79	76, 78	eleqtrrd 2489	. . . . . 6 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A e. ( R1 ` B ) )
80		trss 4279	. . . . . 6 |- ( Tr ( R1 ` B ) -> ( ~P A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) ) )
81	38, 79, 80	mpsyl 61	. . . . 5 |- ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A C_ ( R1 ` B ) )
82	81	ex 424	. . . 4 |- ( A e. ( R1 ` B ) -> ( Lim B -> ~P A C_ ( R1 ` B ) ) )
83	82	adantld 454	. . 3 |- ( A e. ( R1 ` B ) -> ( ( B e. _V /\ Lim B ) -> ~P A C_ ( R1 ` B ) ) )
84	18, 37, 83	3jaod 1248	. 2 |- ( A e. ( R1 ` B ) -> ( ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) -> ~P A C_ ( R1 ` B ) ) )
85	10, 84	mpd 15	1 |- ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   \/ w3o 935   = wceq 1649   e. wcel 1721   E.wrex 2675   _Vcvv 2924   C_ wss 3288   (/)c0 3596   ~Pcpw 3767   U_ciun 4061   Tr wtr 4270   Ord word 4548   Oncon0 4549   Lim wlim 4550   suc csuc 4551   dom cdm 4845   Fun wfun 5415   ` cfv 5421   R1cr1 7652

This theorem is referenced by:  r1sscl  7675

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 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668

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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-recs 6600  df-rdg 6635  df-r1 7654