Proof of Theorem rankpwi
Step | Hyp | Ref
| Expression |
1 | | rankidn 9317 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) |
2 | | rankon 9290 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
3 | | r1suc 9265 |
. . . . . . 7
⊢
((rank‘𝐴)
∈ On → (𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴))) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) = 𝒫
(𝑅1‘(rank‘𝐴)) |
5 | 4 | eleq2i 2824 |
. . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴))) |
6 | | elpwi 4494 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘(rank‘𝐴)) → 𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
7 | | pwidg 4507 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ 𝒫 𝐴) |
8 | | ssel 3868 |
. . . . . 6
⊢
(𝒫 𝐴 ⊆
(𝑅1‘(rank‘𝐴)) → (𝐴 ∈ 𝒫 𝐴 → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
9 | 6, 7, 8 | syl2imc 41 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈ 𝒫
(𝑅1‘(rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
10 | 5, 9 | syl5bi 245 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝒫
𝐴 ∈
(𝑅1‘suc (rank‘𝐴)) → 𝐴 ∈
(𝑅1‘(rank‘𝐴)))) |
11 | 1, 10 | mtod 201 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬
𝒫 𝐴 ∈
(𝑅1‘suc (rank‘𝐴))) |
12 | | r1rankidb 9299 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
13 | 12 | sspwd 4500 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆ 𝒫
(𝑅1‘(rank‘𝐴))) |
14 | 13, 4 | sseqtrrdi 3926 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ⊆
(𝑅1‘suc (rank‘𝐴))) |
15 | | fvex 6681 |
. . . . . 6
⊢
(𝑅1‘suc (rank‘𝐴)) ∈ V |
16 | 15 | elpw2 5210 |
. . . . 5
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc (rank‘𝐴)) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
(rank‘𝐴))) |
17 | 14, 16 | sylibr 237 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈ 𝒫
(𝑅1‘suc (rank‘𝐴))) |
18 | 2 | onsuci 7566 |
. . . . 5
⊢ suc
(rank‘𝐴) ∈
On |
19 | | r1suc 9265 |
. . . . 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 2844 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈
(𝑅1‘suc suc (rank‘𝐴))) |
22 | | pwwf 9302 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) |
23 | | rankr1c 9316 |
. . . 4
⊢
(𝒫 𝐴 ∈
∪ (𝑅1 “ On) → (suc
(rank‘𝐴) =
(rank‘𝒫 𝐴)
↔ (¬ 𝒫 𝐴
∈ (𝑅1‘suc (rank‘𝐴)) ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
(rank‘𝐴))))) |
24 | 22, 23 | sylbi 220 |
. . 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 2744 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) |