This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ ( rank ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )

Proof

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