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 ‘ 𝐵 ) ) )