Proof of Theorem rankpwi
Step | Hyp | Ref
| Expression |
1 | | rankidn 8568 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) |
2 | | rankon 8541 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
3 | | r1suc 8516 |
. . . . . . 7
⊢
((rank‘𝐴)
∈ On → (𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴))) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴)) |
5 | 4 | eleq2i 2680 |
. . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴))) |
6 | | elpwi 4117 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘(rank‘𝐴)) → 𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
7 | | pwidg 4121 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ 𝒫 𝐴) |
8 | | ssel 3562 |
. . . . . 6
⊢
(𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴)) → (𝐴 ∈ 𝒫 𝐴 → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
9 | 6, 7, 8 | syl2imc 40 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
10 | 5, 9 | syl5bi 231 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
11 | 1, 10 | mtod 188 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬
𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴))) |
12 | | r1rankidb 8550 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
13 | | sspwb 4844 |
. . . . . . 7
⊢ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ↔ 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘(rank‘𝐴))) |
14 | 12, 13 | sylib 207 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆ 𝒫
(𝑅1‘(rank‘𝐴))) |
15 | 14, 4 | syl6sseqr 3615 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆
(𝑅1‘suc (rank‘𝐴))) |
16 | | fvex 6113 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) ∈ V |
17 | 16 | elpw2 4755 |
. . . . 5
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
(rank‘𝐴))) |
18 | 15, 17 | sylibr 223 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈ 𝒫
(𝑅1‘suc (rank‘𝐴))) |
19 | 2 | onsuci 6930 |
. . . . 5
⊢ suc
(rank‘𝐴) ∈
On |
20 | | r1suc 8516 |
. . . . 5
⊢ (suc
(rank‘𝐴) ∈ On
→ (𝑅1‘suc suc (rank‘𝐴)) = 𝒫
(𝑅1‘suc (rank‘𝐴))) |
21 | 19, 20 | ax-mp 5 |
. . . 4
⊢
(𝑅1‘suc suc (rank‘𝐴)) = 𝒫
(𝑅1‘suc (rank‘𝐴)) |
22 | 18, 21 | syl6eleqr 2699 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈
(𝑅1‘suc suc (rank‘𝐴))) |
23 | | pwwf 8553 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) |
24 | | rankr1c 8567 |
. . . 4
⊢
(𝒫 𝐴 ∈
∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) |
25 | 23, 24 | sylbi 206 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) |
26 | 11, 22, 25 | mpbir2and 959 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)) |
27 | 26 | eqcomd 2616 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) |