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 ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )

Proof

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