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 fndm ⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
13 11 12 ax-mp ⊢ dom 𝑅1 = On
14 10 13 eleqtrrdi ⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ dom 𝑅1 )
15 rankr1ag ⊢ ( ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ suc 𝐵 ∈ dom 𝑅1 ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ suc 𝐵 ) )
16 9 14 15 syl2an ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ On ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ suc 𝐵 ) )
17 13 eleq2i ⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On )
18 rankr1ag ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
19 17 18 sylan2br ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
20 7 16 19 3bitr4rd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )
21 20 ex ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )
22 r1elwf ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
23 r1elwf ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
24 r1elssi ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
25 23 24 syl ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝒫 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
26 ssid ⊢ 𝐴 ⊆ 𝐴
27 pwexr ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝐴 ∈ V )
28 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
29 27 28 syl ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → ( 𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
30 26 29 mpbiri ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝐴 ∈ 𝒫 𝐴 )
31 25 30 sseldd ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
32 22 31 pm5.21ni ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )
33 32 a1d ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )
34 21 33 pm2.61i ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )