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 ⁡ B → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ B

Proof

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