Metamath Proof Explorer


Theorem r1pwcl

Description: The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004) (Proof shortened by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1pwcl ( Lim 𝐵 → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 r1elwf ( 𝐴 ∈ ( 𝑅1𝐵 ) → 𝐴 ( 𝑅1 “ On ) )
2 elfvdm ( 𝐴 ∈ ( 𝑅1𝐵 ) → 𝐵 ∈ dom 𝑅1 )
3 1 2 jca ( 𝐴 ∈ ( 𝑅1𝐵 ) → ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) )
4 3 a1i ( Lim 𝐵 → ( 𝐴 ∈ ( 𝑅1𝐵 ) → ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) )
5 r1elwf ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) → 𝒫 𝐴 ( 𝑅1 “ On ) )
6 pwwf ( 𝐴 ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ( 𝑅1 “ On ) )
7 5 6 sylibr ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) → 𝐴 ( 𝑅1 “ On ) )
8 elfvdm ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) → 𝐵 ∈ dom 𝑅1 )
9 7 8 jca ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) → ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) )
10 9 a1i ( Lim 𝐵 → ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) → ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) )
11 limsuc ( Lim 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
12 11 adantr ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
13 rankpwi ( 𝐴 ( 𝑅1 “ On ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )
14 13 ad2antrl ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )
15 14 eleq1d ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
16 12 15 bitr4d ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )
17 rankr1ag ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
18 17 adantl ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
19 rankr1ag ( ( 𝒫 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )
20 6 19 sylanb ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )
21 20 adantl ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )
22 16 18 21 3bitr4d ( ( Lim 𝐵 ∧ ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ) )
23 22 ex ( Lim 𝐵 → ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ) ) )
24 4 10 23 pm5.21ndd ( Lim 𝐵 → ( 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1𝐵 ) ) )