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 ∈ ⋃ R1 On → rank ⁡ 𝒫 A = suc ⁡ rank ⁡ A

Proof

Step Hyp Ref Expression
1 rankidn ⊢ A ∈ ⋃ R1 On → ¬ A ∈ R1 ⁡ rank ⁡ A
2 rankon ⊢ rank ⁡ A ∈ On
3 r1suc ⊢ rank ⁡ A ∈ On → R1 ⁡ suc ⁡ rank ⁡ A = 𝒫 R1 ⁡ rank ⁡ A
4 2 3 ax-mp ⊢ R1 ⁡ suc ⁡ rank ⁡ A = 𝒫 R1 ⁡ rank ⁡ A
5 4 eleq2i ⊢ 𝒫 A ∈ R1 ⁡ suc ⁡ rank ⁡ A ↔ 𝒫 A ∈ 𝒫 R1 ⁡ rank ⁡ A
6 elpwi ⊢ 𝒫 A ∈ 𝒫 R1 ⁡ rank ⁡ A → 𝒫 A ⊆ R1 ⁡ rank ⁡ A
7 pwidg ⊢ A ∈ ⋃ R1 On → A ∈ 𝒫 A
8 ssel ⊢ 𝒫 A ⊆ R1 ⁡ rank ⁡ A → A ∈ 𝒫 A → A ∈ R1 ⁡ rank ⁡ A
9 6 7 8 syl2imc ⊢ A ∈ ⋃ R1 On → 𝒫 A ∈ 𝒫 R1 ⁡ rank ⁡ A → A ∈ R1 ⁡ rank ⁡ A
10 5 9 biimtrid ⊢ A ∈ ⋃ R1 On → 𝒫 A ∈ R1 ⁡ suc ⁡ rank ⁡ A → A ∈ R1 ⁡ rank ⁡ A
11 1 10 mtod ⊢ A ∈ ⋃ R1 On → ¬ 𝒫 A ∈ R1 ⁡ suc ⁡ rank ⁡ A
12 r1rankidb ⊢ A ∈ ⋃ R1 On → A ⊆ R1 ⁡ rank ⁡ A
13 12 sspwd ⊢ A ∈ ⋃ R1 On → 𝒫 A ⊆ 𝒫 R1 ⁡ rank ⁡ A
14 13 4 sseqtrrdi ⊢ A ∈ ⋃ R1 On → 𝒫 A ⊆ R1 ⁡ suc ⁡ rank ⁡ A
15 fvex ⊢ R1 ⁡ suc ⁡ rank ⁡ A ∈ V
16 15 elpw2 ⊢ 𝒫 A ∈ 𝒫 R1 ⁡ suc ⁡ rank ⁡ A ↔ 𝒫 A ⊆ R1 ⁡ suc ⁡ rank ⁡ A
17 14 16 sylibr ⊢ A ∈ ⋃ R1 On → 𝒫 A ∈ 𝒫 R1 ⁡ suc ⁡ rank ⁡ A
18 2 onsuci ⊢ suc ⁡ rank ⁡ A ∈ On
19 r1suc ⊢ suc ⁡ rank ⁡ A ∈ On → R1 ⁡ suc ⁡ suc ⁡ rank ⁡ A = 𝒫 R1 ⁡ suc ⁡ rank ⁡ A
20 18 19 ax-mp ⊢ R1 ⁡ suc ⁡ suc ⁡ rank ⁡ A = 𝒫 R1 ⁡ suc ⁡ rank ⁡ A
21 17 20 eleqtrrdi ⊢ A ∈ ⋃ R1 On → 𝒫 A ∈ R1 ⁡ suc ⁡ suc ⁡ rank ⁡ A
22 pwwf ⊢ A ∈ ⋃ R1 On ↔ 𝒫 A ∈ ⋃ R1 On
23 rankr1c ⊢ 𝒫 A ∈ ⋃ R1 On → suc ⁡ rank ⁡ A = rank ⁡ 𝒫 A ↔ ¬ 𝒫 A ∈ R1 ⁡ suc ⁡ rank ⁡ A ∧ 𝒫 A ∈ R1 ⁡ suc ⁡ suc ⁡ rank ⁡ A
24 22 23 sylbi ⊢ A ∈ ⋃ R1 On → suc ⁡ rank ⁡ A = rank ⁡ 𝒫 A ↔ ¬ 𝒫 A ∈ R1 ⁡ suc ⁡ rank ⁡ A ∧ 𝒫 A ∈ R1 ⁡ suc ⁡ suc ⁡ rank ⁡ A
25 11 21 24 mpbir2and ⊢ A ∈ ⋃ R1 On → suc ⁡ rank ⁡ A = rank ⁡ 𝒫 A
26 25 eqcomd ⊢ A ∈ ⋃ R1 On → rank ⁡ 𝒫 A = suc ⁡ rank ⁡ A