Proof of Theorem r1pw
Step | Hyp | Ref
| Expression |
1 | | rankpwi 8963 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) |
2 | 1 | eleq1d 2891 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
((rank‘𝒫 𝐴)
∈ suc 𝐵 ↔ suc
(rank‘𝐴) ∈ suc
𝐵)) |
3 | | eloni 5973 |
. . . . . . 7
⊢ (𝐵 ∈ On → Ord 𝐵) |
4 | | ordsucelsuc 7283 |
. . . . . . 7
⊢ (Ord
𝐵 → ((rank‘𝐴) ∈ 𝐵 ↔ suc (rank‘𝐴) ∈ suc 𝐵)) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝐵 ∈ On →
((rank‘𝐴) ∈
𝐵 ↔ suc
(rank‘𝐴) ∈ suc
𝐵)) |
6 | 5 | bicomd 215 |
. . . . 5
⊢ (𝐵 ∈ On → (suc
(rank‘𝐴) ∈ suc
𝐵 ↔ (rank‘𝐴) ∈ 𝐵)) |
7 | 2, 6 | sylan9bb 507 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ On) →
((rank‘𝒫 𝐴)
∈ suc 𝐵 ↔
(rank‘𝐴) ∈ 𝐵)) |
8 | | pwwf 8947 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) |
9 | 8 | biimpi 208 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) |
10 | | suceloni 7274 |
. . . . . 6
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
11 | | r1fnon 8907 |
. . . . . . 7
⊢
𝑅1 Fn On |
12 | | fndm 6223 |
. . . . . . 7
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
14 | 10, 13 | syl6eleqr 2917 |
. . . . 5
⊢ (𝐵 ∈ On → suc 𝐵 ∈ dom
𝑅1) |
15 | | rankr1ag 8942 |
. . . . 5
⊢
((𝒫 𝐴 ∈
∪ (𝑅1 “ On) ∧ suc 𝐵 ∈ dom
𝑅1) → (𝒫 𝐴 ∈ (𝑅1‘suc
𝐵) ↔
(rank‘𝒫 𝐴)
∈ suc 𝐵)) |
16 | 9, 14, 15 | syl2an 591 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ On) → (𝒫
𝐴 ∈
(𝑅1‘suc 𝐵) ↔ (rank‘𝒫 𝐴) ∈ suc 𝐵)) |
17 | 13 | eleq2i 2898 |
. . . . 5
⊢ (𝐵 ∈ dom
𝑅1 ↔ 𝐵 ∈ On) |
18 | | rankr1ag 8942 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) |
19 | 17, 18 | sylan2br 590 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ On) → (𝐴 ∈
(𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) |
20 | 7, 16, 19 | 3bitr4rd 304 |
. . 3
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ On) → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc
𝐵))) |
21 | 20 | ex 403 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 ∈ On → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc
𝐵)))) |
22 | | r1elwf 8936 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
23 | | r1elwf 8936 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → 𝒫 𝐴 ∈ ∪
(𝑅1 “ On)) |
24 | | r1elssi 8945 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
∪ (𝑅1 “ On) →
𝒫 𝐴 ⊆ ∪ (𝑅1 “ On)) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → 𝒫 𝐴 ⊆ ∪
(𝑅1 “ On)) |
26 | | ssid 3848 |
. . . . . 6
⊢ 𝐴 ⊆ 𝐴 |
27 | | pwexr 7234 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → 𝐴 ∈ V) |
28 | | elpwg 4386 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
30 | 26, 29 | mpbiri 250 |
. . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → 𝐴 ∈ 𝒫 𝐴) |
31 | 25, 30 | sseldd 3828 |
. . . 4
⊢
(𝒫 𝐴 ∈
(𝑅1‘suc 𝐵) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
32 | 22, 31 | pm5.21ni 369 |
. . 3
⊢ (¬
𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc
𝐵))) |
33 | 32 | a1d 25 |
. 2
⊢ (¬
𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 ∈ On → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc
𝐵)))) |
34 | 21, 33 | pm2.61i 177 |
1
⊢ (𝐵 ∈ On → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc
𝐵))) |