Proof of Theorem mappwen
Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . . 5
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 𝐴 ≼ 𝒫 𝐵) |
2 | | pw2eng 8066 |
. . . . . 6
⊢ (𝐵 ∈ dom card →
𝒫 𝐵 ≈
(2𝑜 ↑𝑚 𝐵)) |
3 | 2 | ad2antrr 762 |
. . . . 5
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 𝒫 𝐵 ≈ (2𝑜
↑𝑚 𝐵)) |
4 | | domentr 8015 |
. . . . 5
⊢ ((𝐴 ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ≈ (2𝑜
↑𝑚 𝐵)) → 𝐴 ≼ (2𝑜
↑𝑚 𝐵)) |
5 | 1, 3, 4 | syl2anc 693 |
. . . 4
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 𝐴 ≼ (2𝑜
↑𝑚 𝐵)) |
6 | | mapdom1 8125 |
. . . 4
⊢ (𝐴 ≼ (2𝑜
↑𝑚 𝐵) → (𝐴 ↑𝑚 𝐵) ≼
((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵)) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (𝐴 ↑𝑚 𝐵) ≼
((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵)) |
8 | | 2on 7568 |
. . . . . . 7
⊢
2𝑜 ∈ On |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 2𝑜 ∈
On) |
10 | | simpll 790 |
. . . . . 6
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 𝐵 ∈ dom card) |
11 | | mapxpen 8126 |
. . . . . 6
⊢
((2𝑜 ∈ On ∧ 𝐵 ∈ dom card ∧ 𝐵 ∈ dom card) →
((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 (𝐵 × 𝐵))) |
12 | 9, 10, 10, 11 | syl3anc 1326 |
. . . . 5
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 (𝐵 × 𝐵))) |
13 | 8 | elexi 3213 |
. . . . . . 7
⊢
2𝑜 ∈ V |
14 | 13 | enref 7988 |
. . . . . 6
⊢
2𝑜 ≈ 2𝑜 |
15 | | infxpidm2 8840 |
. . . . . . 7
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵) → (𝐵 × 𝐵) ≈ 𝐵) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (𝐵 × 𝐵) ≈ 𝐵) |
17 | | mapen 8124 |
. . . . . 6
⊢
((2𝑜 ≈ 2𝑜 ∧ (𝐵 × 𝐵) ≈ 𝐵) → (2𝑜
↑𝑚 (𝐵 × 𝐵)) ≈ (2𝑜
↑𝑚 𝐵)) |
18 | 14, 16, 17 | sylancr 695 |
. . . . 5
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (2𝑜
↑𝑚 (𝐵 × 𝐵)) ≈ (2𝑜
↑𝑚 𝐵)) |
19 | | entr 8008 |
. . . . 5
⊢
((((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 (𝐵 × 𝐵)) ∧ (2𝑜
↑𝑚 (𝐵 × 𝐵)) ≈ (2𝑜
↑𝑚 𝐵)) → ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 𝐵)) |
20 | 12, 18, 19 | syl2anc 693 |
. . . 4
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 𝐵)) |
21 | 3 | ensymd 8007 |
. . . 4
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (2𝑜
↑𝑚 𝐵) ≈ 𝒫 𝐵) |
22 | | entr 8008 |
. . . 4
⊢
((((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵) ≈ (2𝑜
↑𝑚 𝐵) ∧ (2𝑜
↑𝑚 𝐵) ≈ 𝒫 𝐵) → ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
23 | 20, 21, 22 | syl2anc 693 |
. . 3
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
24 | | domentr 8015 |
. . 3
⊢ (((𝐴 ↑𝑚
𝐵) ≼
((2𝑜 ↑𝑚 𝐵) ↑𝑚 𝐵) ∧ ((2𝑜
↑𝑚 𝐵) ↑𝑚 𝐵) ≈ 𝒫 𝐵) → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
25 | 7, 23, 24 | syl2anc 693 |
. 2
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
26 | | mapdom1 8125 |
. . . 4
⊢
(2𝑜 ≼ 𝐴 → (2𝑜
↑𝑚 𝐵) ≼ (𝐴 ↑𝑚 𝐵)) |
27 | 26 | ad2antrl 764 |
. . 3
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (2𝑜
↑𝑚 𝐵) ≼ (𝐴 ↑𝑚 𝐵)) |
28 | | endomtr 8014 |
. . 3
⊢
((𝒫 𝐵
≈ (2𝑜 ↑𝑚 𝐵) ∧ (2𝑜
↑𝑚 𝐵) ≼ (𝐴 ↑𝑚 𝐵)) → 𝒫 𝐵 ≼ (𝐴 ↑𝑚 𝐵)) |
29 | 3, 27, 28 | syl2anc 693 |
. 2
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → 𝒫 𝐵 ≼ (𝐴 ↑𝑚 𝐵)) |
30 | | sbth 8080 |
. 2
⊢ (((𝐴 ↑𝑚
𝐵) ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ≼ (𝐴 ↑𝑚 𝐵)) → (𝐴 ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
31 | 25, 29, 30 | syl2anc 693 |
1
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (𝐴 ↑𝑚 𝐵) ≈ 𝒫 𝐵) |