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 12 sspwd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
14 13 4 sseqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
15 fvex ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ V
16 15 elpw2 ⊢ ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
17 14 16 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
18 2 onsuci ⊢ suc ( rank ‘ 𝐴 ) ∈ On
19 r1suc ⊢ ( suc ( rank ‘ 𝐴 ) ∈ On → ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
20 18 19 ax-mp ⊢ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
21 17 20 eleqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) )
22 pwwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
23 rankr1c ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) ↔ ( ¬ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∧ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) ) ) )
24 22 23 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) ↔ ( ¬ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∧ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) ) ) )
25 11 21 24 mpbir2and ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) = ( rank ‘ 𝒫 𝐴 ) )
26 25 eqcomd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )