Metamath Proof Explorer


Theorem r1pwss

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

Ref Expression
Assertion r1pwss AR1B𝒫AR1B

Proof

Step Hyp Ref Expression
1 r1funlim FunR1LimdomR1
2 1 simpri LimdomR1
3 limord LimdomR1OrddomR1
4 2 3 ax-mp OrddomR1
5 ordsson OrddomR1domR1On
6 4 5 ax-mp domR1On
7 elfvdm AR1BBdomR1
8 6 7 sselid AR1BBOn
9 onzsl BOnB=xOnB=sucxBVLimB
10 8 9 sylib AR1BB=xOnB=sucxBVLimB
11 noel ¬A
12 fveq2 B=R1B=R1
13 r10 R1=
14 12 13 eqtrdi B=R1B=
15 14 eleq2d B=AR1BA
16 15 biimpcd AR1BB=A
17 11 16 mtoi AR1B¬B=
18 17 pm2.21d AR1BB=𝒫AR1B
19 simpl AR1BB=sucxAR1B
20 simpr AR1BB=sucxB=sucx
21 20 fveq2d AR1BB=sucxR1B=R1sucx
22 7 adantr AR1BB=sucxBdomR1
23 20 22 eqeltrrd AR1BB=sucxsucxdomR1
24 limsuc LimdomR1xdomR1sucxdomR1
25 2 24 ax-mp xdomR1sucxdomR1
26 23 25 sylibr AR1BB=sucxxdomR1
27 r1sucg xdomR1R1sucx=𝒫R1x
28 26 27 syl AR1BB=sucxR1sucx=𝒫R1x
29 21 28 eqtrd AR1BB=sucxR1B=𝒫R1x
30 19 29 eleqtrd AR1BB=sucxA𝒫R1x
31 elpwi A𝒫R1xAR1x
32 sspw AR1x𝒫A𝒫R1x
33 30 31 32 3syl AR1BB=sucx𝒫A𝒫R1x
34 33 29 sseqtrrd AR1BB=sucx𝒫AR1B
35 34 ex AR1BB=sucx𝒫AR1B
36 35 rexlimdvw AR1BxOnB=sucx𝒫AR1B
37 r1tr TrR1B
38 simpl AR1BLimBAR1B
39 r1limg BdomR1LimBR1B=xBR1x
40 7 39 sylan AR1BLimBR1B=xBR1x
41 38 40 eleqtrd AR1BLimBAxBR1x
42 eliun AxBR1xxBAR1x
43 41 42 sylib AR1BLimBxBAR1x
44 simprl AR1BLimBxBAR1xxB
45 limsuc LimBxBsucxB
46 45 ad2antlr AR1BLimBxBAR1xxBsucxB
47 44 46 mpbid AR1BLimBxBAR1xsucxB
48 limsuc LimBsucxBsucsucxB
49 48 ad2antlr AR1BLimBxBAR1xsucxBsucsucxB
50 47 49 mpbid AR1BLimBxBAR1xsucsucxB
51 r1tr TrR1x
52 simprr AR1BLimBxBAR1xAR1x
53 trss TrR1xAR1xAR1x
54 51 52 53 mpsyl AR1BLimBxBAR1xAR1x
55 54 32 syl AR1BLimBxBAR1x𝒫A𝒫R1x
56 7 ad2antrr AR1BLimBxBAR1xBdomR1
57 ordtr1 OrddomR1xBBdomR1xdomR1
58 4 57 ax-mp xBBdomR1xdomR1
59 44 56 58 syl2anc AR1BLimBxBAR1xxdomR1
60 59 27 syl AR1BLimBxBAR1xR1sucx=𝒫R1x
61 55 60 sseqtrrd AR1BLimBxBAR1x𝒫AR1sucx
62 fvex R1sucxV
63 62 elpw2 𝒫A𝒫R1sucx𝒫AR1sucx
64 61 63 sylibr AR1BLimBxBAR1x𝒫A𝒫R1sucx
65 59 25 sylib AR1BLimBxBAR1xsucxdomR1
66 r1sucg sucxdomR1R1sucsucx=𝒫R1sucx
67 65 66 syl AR1BLimBxBAR1xR1sucsucx=𝒫R1sucx
68 64 67 eleqtrrd AR1BLimBxBAR1x𝒫AR1sucsucx
69 fveq2 y=sucsucxR1y=R1sucsucx
70 69 eleq2d y=sucsucx𝒫AR1y𝒫AR1sucsucx
71 70 rspcev sucsucxB𝒫AR1sucsucxyB𝒫AR1y
72 50 68 71 syl2anc AR1BLimBxBAR1xyB𝒫AR1y
73 43 72 rexlimddv AR1BLimByB𝒫AR1y
74 eliun 𝒫AyBR1yyB𝒫AR1y
75 73 74 sylibr AR1BLimB𝒫AyBR1y
76 r1limg BdomR1LimBR1B=yBR1y
77 7 76 sylan AR1BLimBR1B=yBR1y
78 75 77 eleqtrrd AR1BLimB𝒫AR1B
79 trss TrR1B𝒫AR1B𝒫AR1B
80 37 78 79 mpsyl AR1BLimB𝒫AR1B
81 80 ex AR1BLimB𝒫AR1B
82 81 adantld AR1BBVLimB𝒫AR1B
83 18 36 82 3jaod AR1BB=xOnB=sucxBVLimB𝒫AR1B
84 10 83 mpd AR1B𝒫AR1B