Metamath Proof Explorer

Theorem r1pw

Description: A set is in a given stage of the cumulative hierarchy of sets if and only if its powerset is in the successor stage. (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 onsuc ⊢ ( 𝐵 ∈ 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 𝐵 ) ) )