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 ‘ 𝒫 𝐴 ) ∈ 𝐵 ) )