Proof of Theorem rankpwi
Step | Hyp | Ref
| Expression |
1 | | rankidn 9580 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) |
2 | | rankon 9553 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
3 | | r1suc 9528 |
. . . . . . 7
⊢
((rank‘𝐴)
∈ On → (𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴))) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴)) |
5 | 4 | eleq2i 2830 |
. . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴))) |
6 | | elpwi 4542 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘(rank‘𝐴)) → 𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
7 | | pwidg 4555 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ 𝒫 𝐴) |
8 | | ssel 3914 |
. . . . . 6
⊢
(𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴)) → (𝐴 ∈ 𝒫 𝐴 → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
9 | 6, 7, 8 | syl2imc 41 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
10 | 5, 9 | syl5bi 241 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
11 | 1, 10 | mtod 197 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬
𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴))) |
12 | | r1rankidb 9562 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
13 | 12 | sspwd 4548 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆ 𝒫
(𝑅1‘(rank‘𝐴))) |
14 | 13, 4 | sseqtrrdi 3972 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆
(𝑅1‘suc (rank‘𝐴))) |
15 | | fvex 6787 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) ∈ V |
16 | 15 | elpw2 5269 |
. . . . 5
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
(rank‘𝐴))) |
17 | 14, 16 | sylibr 233 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈ 𝒫
(𝑅1‘suc (rank‘𝐴))) |
18 | 2 | onsuci 7685 |
. . . . 5
⊢ suc
(rank‘𝐴) ∈
On |
19 | | r1suc 9528 |
. . . . 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 2850 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈
(𝑅1‘suc suc (rank‘𝐴))) |
22 | | pwwf 9565 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) |
23 | | rankr1c 9579 |
. . . 4
⊢
(𝒫 𝐴 ∈
∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) |
24 | 22, 23 | sylbi 216 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) |
25 | 11, 21, 24 | mpbir2and 710 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)) |
26 | 25 | eqcomd 2744 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) |