Metamath Proof Explorer

Theorem rankpwi

Description: The rank of a power set. Part of Exercise 30 of Enderton p. 207. (Contributed by Mario Carneiro, 3-Jun-2013)

Ref Expression
Assertion rankpwi ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rankidn ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
2 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
3 r1suc ⊢ ( ( rank ‘ 𝐴 ) ∈ On → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
4 2 3 ax-mp ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
5 4 eleq2i ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
6 elpwi ⊢ ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
7 pwidg ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ 𝒫 𝐴 )
8 ssel ⊢ ( 𝒫 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( 𝐴 ∈ 𝒫 𝐴 → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
9 6 7 8 syl2imc ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
10 5 9 syl5bi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
11 1 10 mtod ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
12 r1rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
13 sspwb ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
14 12 13 sylib ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
15 14 4 sseqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
16 fvex ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ V
17 16 elpw2 ⊢ ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
18 15 17 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
19 2 onsuci ⊢ suc ( rank ‘ 𝐴 ) ∈ On
20 r1suc ⊢ ( suc ( rank ‘ 𝐴 ) ∈ On → ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
21 19 20 ax-mp ⊢ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
22 18 21 eleqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) )
23 pwwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
24 rankr1c ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) ↔ ( ¬ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∧ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) ) ) )
25 23 24 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) ↔ ( ¬ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∧ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) ) ) )
26 11 22 25 mpbir2and ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) )
27 26 eqcomd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )