Proof of Theorem rankpwi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rankidn 9862 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) | 
| 2 |  | rankon 9835 | . . . . . . 7
⊢
(rank‘𝐴)
∈ On | 
| 3 |  | r1suc 9810 | . . . . . . 7
⊢
((rank‘𝐴)
∈ On → (𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴))) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴)) | 
| 5 | 4 | eleq2i 2833 | . . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴))) | 
| 6 |  | elpwi 4607 | . . . . . 6
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘(rank‘𝐴)) → 𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) | 
| 7 |  | pwidg 4620 | . . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ 𝒫 𝐴) | 
| 8 |  | ssel 3977 | . . . . . 6
⊢
(𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴)) → (𝐴 ∈ 𝒫 𝐴 → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) | 
| 9 | 6, 7, 8 | syl2imc 41 | . . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) | 
| 10 | 5, 9 | biimtrid 242 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) | 
| 11 | 1, 10 | mtod 198 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬
𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴))) | 
| 12 |  | r1rankidb 9844 | . . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) | 
| 13 | 12 | sspwd 4613 | . . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆ 𝒫
(𝑅1‘(rank‘𝐴))) | 
| 14 | 13, 4 | sseqtrrdi 4025 | . . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆
(𝑅1‘suc (rank‘𝐴))) | 
| 15 |  | fvex 6919 | . . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) ∈ V | 
| 16 | 15 | elpw2 5334 | . . . . 5
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
(rank‘𝐴))) | 
| 17 | 14, 16 | sylibr 234 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈ 𝒫
(𝑅1‘suc (rank‘𝐴))) | 
| 18 | 2 | onsuci 7859 | . . . . 5
⊢ suc
(rank‘𝐴) ∈
On | 
| 19 |  | r1suc 9810 | . . . . 5
⊢ (suc
(rank‘𝐴) ∈ On
→ (𝑅1‘suc suc (rank‘𝐴)) = 𝒫
(𝑅1‘suc (rank‘𝐴))) | 
| 20 | 18, 19 | ax-mp 5 | . . . 4
⊢
(𝑅1‘suc suc (rank‘𝐴)) = 𝒫
(𝑅1‘suc (rank‘𝐴)) | 
| 21 | 17, 20 | eleqtrrdi 2852 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈
(𝑅1‘suc suc (rank‘𝐴))) | 
| 22 |  | pwwf 9847 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) | 
| 23 |  | rankr1c 9861 | . . . 4
⊢
(𝒫 𝐴 ∈
∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) | 
| 24 | 22, 23 | sylbi 217 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) | 
| 25 | 11, 21, 24 | mpbir2and 713 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)) | 
| 26 | 25 | eqcomd 2743 | 1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) |