Metamath Proof Explorer

Theorem r1pw

Description: A stronger property of R1 than rankpw . 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)

Ref Expression
Assertion r1pw ⊢B∈On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B

Proof

Step Hyp Ref Expression
1 rankpwi ⊢A∈⋃R1On→rank⁡𝒫A=suc⁡rank⁡A
2 1 eleq1d ⊢A∈⋃R1On→rank⁡𝒫A∈suc⁡B↔suc⁡rank⁡A∈suc⁡B
3 eloni ⊢B∈On→Ord⁡B
4 ordsucelsuc ⊢Ord⁡B→rank⁡A∈B↔suc⁡rank⁡A∈suc⁡B
5 3 4 syl ⊢B∈On→rank⁡A∈B↔suc⁡rank⁡A∈suc⁡B
6 5 bicomd ⊢B∈On→suc⁡rank⁡A∈suc⁡B↔rank⁡A∈B
7 2 6 sylan9bb ⊢A∈⋃R1On∧B∈On→rank⁡𝒫A∈suc⁡B↔rank⁡A∈B
8 pwwf ⊢A∈⋃R1On↔𝒫A∈⋃R1On
9 8 biimpi ⊢A∈⋃R1On→𝒫A∈⋃R1On
10 onsuc ⊢B∈On→suc⁡B∈On
11 r1fnon ⊢R1FnOn
12 11 fndmi ⊢dom⁡R1=On
13 10 12 eleqtrrdi ⊢B∈On→suc⁡B∈dom⁡R1
14 rankr1ag ⊢𝒫A∈⋃R1On∧suc⁡B∈dom⁡R1→𝒫A∈R1⁡suc⁡B↔rank⁡𝒫A∈suc⁡B
15 9 13 14 syl2an ⊢A∈⋃R1On∧B∈On→𝒫A∈R1⁡suc⁡B↔rank⁡𝒫A∈suc⁡B
16 12 eleq2i ⊢B∈dom⁡R1↔B∈On
17 rankr1ag ⊢A∈⋃R1On∧B∈dom⁡R1→A∈R1⁡B↔rank⁡A∈B
18 16 17 sylan2br ⊢A∈⋃R1On∧B∈On→A∈R1⁡B↔rank⁡A∈B
19 7 15 18 3bitr4rd ⊢A∈⋃R1On∧B∈On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B
20 19 ex ⊢A∈⋃R1On→B∈On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B
21 r1elwf ⊢A∈R1⁡B→A∈⋃R1On
22 r1elwf ⊢𝒫A∈R1⁡suc⁡B→𝒫A∈⋃R1On
23 r1elssi ⊢𝒫A∈⋃R1On→𝒫A⊆⋃R1On
24 22 23 syl ⊢𝒫A∈R1⁡suc⁡B→𝒫A⊆⋃R1On
25 ssid ⊢A⊆A
26 pwexr ⊢𝒫A∈R1⁡suc⁡B→A∈V
27 elpwg ⊢A∈V→A∈𝒫A↔A⊆A
28 26 27 syl ⊢𝒫A∈R1⁡suc⁡B→A∈𝒫A↔A⊆A
29 25 28 mpbiri ⊢𝒫A∈R1⁡suc⁡B→A∈𝒫A
30 24 29 sseldd ⊢𝒫A∈R1⁡suc⁡B→A∈⋃R1On
31 21 30 pm5.21ni ⊢¬A∈⋃R1On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B
32 31 a1d ⊢¬A∈⋃R1On→B∈On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B
33 20 32 pm2.61i ⊢B∈On→A∈R1⁡B↔𝒫A∈R1⁡suc⁡B