Theorem r1pw 8268

Description: A stronger property of R1 than rankpw 8266. The latter merely proves that R1 of the successor is a power set, but here we prove that if A is in the cumulative hierarchy, then ~P A is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
r1pw	|- ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )

Proof of Theorem r1pw

Step	Hyp	Ref	Expression
1		rankpwi 8246	. . . . . 6 |- ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )
2	1	eleq1d 2490	. . . . 5 |- ( A e. U. ( R1 " On ) -> ( ( rank ` ~P A ) e. suc B <-> suc ( rank ` A ) e. suc B ) )
3		eloni 5395	. . . . . . 7 |- ( B e. On -> Ord B )
4		ordsucelsuc 6607	. . . . . . 7 |- ( Ord B -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. suc B ) )
5	3, 4	syl 17	. . . . . 6 |- ( B e. On -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. suc B ) )
6	5	bicomd 204	. . . . 5 |- ( B e. On -> ( suc ( rank ` A ) e. suc B <-> ( rank ` A ) e. B ) )
7	2, 6	sylan9bb 704	. . . 4 |- ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( ( rank ` ~P A ) e. suc B <-> ( rank ` A ) e. B ) )
8		pwwf 8230	. . . . . 6 |- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
9	8	biimpi 197	. . . . 5 |- ( A e. U. ( R1 " On ) -> ~P A e. U. ( R1 " On ) )
10		suceloni 6598	. . . . . 6 |- ( B e. On -> suc B e. On )
11		r1fnon 8190	. . . . . . 7 |- R1 Fn On
12		fndm 5636	. . . . . . 7 |- ( R1 Fn On -> dom R1 = On )
13	11, 12	ax-mp 5	. . . . . 6 |- dom R1 = On
14	10, 13	syl6eleqr 2517	. . . . 5 |- ( B e. On -> suc B e. dom R1 )
15		rankr1ag 8225	. . . . 5 |- ( ( ~P A e. U. ( R1 " On ) /\ suc B e. dom R1 ) -> ( ~P A e. ( R1 ` suc B ) <-> ( rank ` ~P A ) e. suc B ) )
16	9, 14, 15	syl2an 479	. . . 4 |- ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( ~P A e. ( R1 ` suc B ) <-> ( rank ` ~P A ) e. suc B ) )
17	13	eleq2i 2498	. . . . 5 |- ( B e. dom R1 <-> B e. On )
18		rankr1ag 8225	. . . . 5 |- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
19	17, 18	sylan2br 478	. . . 4 |- ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
20	7, 16, 19	3bitr4rd 289	. . 3 |- ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )
21	20	ex 435	. 2 |- ( A e. U. ( R1 " On ) -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
22		r1elwf 8219	. . . 4 |- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
23		r1elwf 8219	. . . . . 6 |- ( ~P A e. ( R1 ` suc B ) -> ~P A e. U. ( R1 " On ) )
24		r1elssi 8228	. . . . . 6 |- ( ~P A e. U. ( R1 " On ) -> ~P A C_ U. ( R1 " On ) )
25	23, 24	syl 17	. . . . 5 |- ( ~P A e. ( R1 ` suc B ) -> ~P A C_ U. ( R1 " On ) )
26		ssid 3426	. . . . . 6 |- A C_ A
27		elex 3031	. . . . . . . 8 |- ( ~P A e. ( R1 ` suc B ) -> ~P A e. _V )
28		pwexb 6560	. . . . . . . 8 |- ( A e. _V <-> ~P A e. _V )
29	27, 28	sylibr 215	. . . . . . 7 |- ( ~P A e. ( R1 ` suc B ) -> A e. _V )
30		elpwg 3932	. . . . . . 7 |- ( A e. _V -> ( A e. ~P A <-> A C_ A ) )
31	29, 30	syl 17	. . . . . 6 |- ( ~P A e. ( R1 ` suc B ) -> ( A e. ~P A <-> A C_ A ) )
32	26, 31	mpbiri 236	. . . . 5 |- ( ~P A e. ( R1 ` suc B ) -> A e. ~P A )
33	25, 32	sseldd 3408	. . . 4 |- ( ~P A e. ( R1 ` suc B ) -> A e. U. ( R1 " On ) )
34	22, 33	pm5.21ni 353	. . 3 |- ( -. A e. U. ( R1 " On ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )
35	34	a1d 26	. 2 |- ( -. A e. U. ( R1 " On ) -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
36	21, 35	pm2.61i 167	1 |- ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   _Vcvv 3022   C_ wss 3379   ~Pcpw 3924   U.cuni 4162   dom cdm 4796   "cima 4799   Ord word 5384   Oncon0 5385   suc csuc 5387   Fn wfn 5539   ` cfv 5544   R1cr1 8185   rankcrnk 8186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-om 6651  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-r1 8187  df-rank 8188

This theorem is referenced by:  inatsk  9154