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