Metamath Proof Explorer

Theorem ranklim

Description: The rank of a set belongs to a limit ordinal iff the rank of its power set does. (Contributed by NM, 18-Sep-2006)

Ref Expression
Assertion ranklim ⊢ Lim ⁡ B → rank ⁡ A ∈ B ↔ rank ⁡ 𝒫 A ∈ B

Proof

Step Hyp Ref Expression
1 limsuc ⊢ Lim ⁡ B → rank ⁡ A ∈ B ↔ suc ⁡ rank ⁡ A ∈ B
2 1 adantl ⊢ A ∈ V ∧ Lim ⁡ B → rank ⁡ A ∈ B ↔ suc ⁡ rank ⁡ A ∈ B
3 pweq ⊢ x = A → 𝒫 x = 𝒫 A
4 3 fveq2d ⊢ x = A → rank ⁡ 𝒫 x = rank ⁡ 𝒫 A
5 fveq2 ⊢ x = A → rank ⁡ x = rank ⁡ A
6 suceq ⊢ rank ⁡ x = rank ⁡ A → suc ⁡ rank ⁡ x = suc ⁡ rank ⁡ A
7 5 6 syl ⊢ x = A → suc ⁡ rank ⁡ x = suc ⁡ rank ⁡ A
8 4 7 eqeq12d ⊢ x = A → rank ⁡ 𝒫 x = suc ⁡ rank ⁡ x ↔ rank ⁡ 𝒫 A = suc ⁡ rank ⁡ A
9 vex ⊢ x ∈ V
10 9 rankpw ⊢ rank ⁡ 𝒫 x = suc ⁡ rank ⁡ x
11 8 10 vtoclg ⊢ A ∈ V → rank ⁡ 𝒫 A = suc ⁡ rank ⁡ A
12 11 eleq1d ⊢ A ∈ V → rank ⁡ 𝒫 A ∈ B ↔ suc ⁡ rank ⁡ A ∈ B
13 12 adantr ⊢ A ∈ V ∧ Lim ⁡ B → rank ⁡ 𝒫 A ∈ B ↔ suc ⁡ rank ⁡ A ∈ B
14 2 13 bitr4d ⊢ A ∈ V ∧ Lim ⁡ B → rank ⁡ A ∈ B ↔ rank ⁡ 𝒫 A ∈ B
15 fvprc ⊢ ¬ A ∈ V → rank ⁡ A = ∅
16 pwexb ⊢ A ∈ V ↔ 𝒫 A ∈ V
17 fvprc ⊢ ¬ 𝒫 A ∈ V → rank ⁡ 𝒫 A = ∅
18 16 17 sylnbi ⊢ ¬ A ∈ V → rank ⁡ 𝒫 A = ∅
19 15 18 eqtr4d ⊢ ¬ A ∈ V → rank ⁡ A = rank ⁡ 𝒫 A
20 19 eleq1d ⊢ ¬ A ∈ V → rank ⁡ A ∈ B ↔ rank ⁡ 𝒫 A ∈ B
21 20 adantr ⊢ ¬ A ∈ V ∧ Lim ⁡ B → rank ⁡ A ∈ B ↔ rank ⁡ 𝒫 A ∈ B
22 14 21 pm2.61ian ⊢ Lim ⁡ B → rank ⁡ A ∈ B ↔ rank ⁡ 𝒫 A ∈ B