# 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 ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \mathrm{rank}\left(𝒫{A}\right)=\mathrm{suc}\mathrm{rank}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 rankidn ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to ¬{A}\in {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
2 rankon ${⊢}\mathrm{rank}\left({A}\right)\in \mathrm{On}$
3 r1suc ${⊢}\mathrm{rank}\left({A}\right)\in \mathrm{On}\to {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)=𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
4 2 3 ax-mp ${⊢}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)=𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
5 4 eleq2i ${⊢}𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)↔𝒫{A}\in 𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
6 elpwi ${⊢}𝒫{A}\in 𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\to 𝒫{A}\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
7 pwidg ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to {A}\in 𝒫{A}$
8 ssel ${⊢}𝒫{A}\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\to \left({A}\in 𝒫{A}\to {A}\in {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\right)$
9 6 7 8 syl2imc ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \left(𝒫{A}\in 𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\to {A}\in {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\right)$
10 5 9 syl5bi ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \left(𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\to {A}\in {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\right)$
11 1 10 mtod ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to ¬𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
12 r1rankidb ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to {A}\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
13 12 sspwd ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to 𝒫{A}\subseteq 𝒫{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
14 13 4 sseqtrrdi ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to 𝒫{A}\subseteq {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
15 fvex ${⊢}{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\in \mathrm{V}$
16 15 elpw2 ${⊢}𝒫{A}\in 𝒫{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)↔𝒫{A}\subseteq {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
17 14 16 sylibr ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to 𝒫{A}\in 𝒫{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
18 2 onsuci ${⊢}\mathrm{suc}\mathrm{rank}\left({A}\right)\in \mathrm{On}$
19 r1suc ${⊢}\mathrm{suc}\mathrm{rank}\left({A}\right)\in \mathrm{On}\to {R}_{1}\left(\mathrm{suc}\mathrm{suc}\mathrm{rank}\left({A}\right)\right)=𝒫{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
20 18 19 ax-mp ${⊢}{R}_{1}\left(\mathrm{suc}\mathrm{suc}\mathrm{rank}\left({A}\right)\right)=𝒫{R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
21 17 20 eleqtrrdi ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to 𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{suc}\mathrm{rank}\left({A}\right)\right)$
22 pwwf ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]↔𝒫{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]$
23 rankr1c ${⊢}𝒫{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \left(\mathrm{suc}\mathrm{rank}\left({A}\right)=\mathrm{rank}\left(𝒫{A}\right)↔\left(¬𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\wedge 𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\right)\right)$
24 22 23 sylbi ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \left(\mathrm{suc}\mathrm{rank}\left({A}\right)=\mathrm{rank}\left(𝒫{A}\right)↔\left(¬𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\wedge 𝒫{A}\in {R}_{1}\left(\mathrm{suc}\mathrm{suc}\mathrm{rank}\left({A}\right)\right)\right)\right)$
25 11 21 24 mpbir2and ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \mathrm{suc}\mathrm{rank}\left({A}\right)=\mathrm{rank}\left(𝒫{A}\right)$
26 25 eqcomd ${⊢}{A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \mathrm{rank}\left(𝒫{A}\right)=\mathrm{suc}\mathrm{rank}\left({A}\right)$