Proof of Theorem hsmexlem1
| Step | Hyp | Ref
| Expression |
| 1 | | hsmexlem.o |
. . . 4
⊢ 𝑂 = OrdIso( E , 𝐴) |
| 2 | 1 | oicl 9569 |
. . 3
⊢ Ord dom
𝑂 |
| 3 | | relwdom 9606 |
. . . . . . . 8
⊢ Rel
≼* |
| 4 | 3 | brrelex1i 5741 |
. . . . . . 7
⊢ (𝐴 ≼* 𝐵 → 𝐴 ∈ V) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ∈ V) |
| 6 | | uniexg 7760 |
. . . . . 6
⊢ (𝐴 ∈ V → ∪ 𝐴
∈ V) |
| 7 | | sucexg 7825 |
. . . . . 6
⊢ (∪ 𝐴
∈ V → suc ∪ 𝐴 ∈ V) |
| 8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → suc ∪ 𝐴
∈ V) |
| 9 | 1 | oif 9570 |
. . . . . . 7
⊢ 𝑂:dom 𝑂⟶𝐴 |
| 10 | | onsucuni 7848 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ⊆ suc ∪
𝐴) |
| 12 | | fss 6752 |
. . . . . . 7
⊢ ((𝑂:dom 𝑂⟶𝐴 ∧ 𝐴 ⊆ suc ∪
𝐴) → 𝑂:dom 𝑂⟶suc ∪
𝐴) |
| 13 | 9, 11, 12 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂:dom 𝑂⟶suc ∪
𝐴) |
| 14 | 1 | oismo 9580 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → (Smo 𝑂 ∧ ran 𝑂 = 𝐴)) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (Smo 𝑂 ∧ ran 𝑂 = 𝐴)) |
| 16 | 15 | simpld 494 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Smo 𝑂) |
| 17 | | ssorduni 7799 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
| 18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Ord ∪ 𝐴) |
| 19 | | ordsuc 7833 |
. . . . . . 7
⊢ (Ord
∪ 𝐴 ↔ Ord suc ∪
𝐴) |
| 20 | 18, 19 | sylib 218 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Ord suc ∪ 𝐴) |
| 21 | | smocdmdom 8408 |
. . . . . 6
⊢ ((𝑂:dom 𝑂⟶suc ∪
𝐴 ∧ Smo 𝑂 ∧ Ord suc ∪ 𝐴)
→ dom 𝑂 ⊆ suc
∪ 𝐴) |
| 22 | 13, 16, 20, 21 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ⊆ suc ∪
𝐴) |
| 23 | 8, 22 | ssexd 5324 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ V) |
| 24 | | elong 6392 |
. . . 4
⊢ (dom
𝑂 ∈ V → (dom
𝑂 ∈ On ↔ Ord dom
𝑂)) |
| 25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (dom 𝑂 ∈ On ↔ Ord dom 𝑂)) |
| 26 | 2, 25 | mpbiri 258 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ On) |
| 27 | | canth2g 9171 |
. . . 4
⊢ (dom
𝑂 ∈ V → dom 𝑂 ≺ 𝒫 dom 𝑂) |
| 28 | | sdomdom 9020 |
. . . 4
⊢ (dom
𝑂 ≺ 𝒫 dom
𝑂 → dom 𝑂 ≼ 𝒫 dom 𝑂) |
| 29 | 23, 27, 28 | 3syl 18 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼ 𝒫 dom 𝑂) |
| 30 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ⊆ On) |
| 31 | | epweon 7795 |
. . . . . . . . . . 11
⊢ E We
On |
| 32 | | wess 5671 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ On → ( E We On
→ E We 𝐴)) |
| 33 | 30, 31, 32 | mpisyl 21 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → E We 𝐴) |
| 34 | | epse 5667 |
. . . . . . . . . 10
⊢ E Se
𝐴 |
| 35 | 1 | oiiso2 9571 |
. . . . . . . . . 10
⊢ (( E We
𝐴 ∧ E Se 𝐴) → 𝑂 Isom E , E (dom 𝑂, ran 𝑂)) |
| 36 | 33, 34, 35 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂 Isom E , E (dom 𝑂, ran 𝑂)) |
| 37 | | isof1o 7343 |
. . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, ran 𝑂) → 𝑂:dom 𝑂–1-1-onto→ran
𝑂) |
| 38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂:dom 𝑂–1-1-onto→ran
𝑂) |
| 39 | 15 | simprd 495 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → ran 𝑂 = 𝐴) |
| 40 | 39 | f1oeq3d 6845 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (𝑂:dom 𝑂–1-1-onto→ran
𝑂 ↔ 𝑂:dom 𝑂–1-1-onto→𝐴)) |
| 41 | 38, 40 | mpbid 232 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂:dom 𝑂–1-1-onto→𝐴) |
| 42 | | f1oen2g 9009 |
. . . . . . 7
⊢ ((dom
𝑂 ∈ On ∧ 𝐴 ∈ V ∧ 𝑂:dom 𝑂–1-1-onto→𝐴) → dom 𝑂 ≈ 𝐴) |
| 43 | 26, 5, 41, 42 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≈ 𝐴) |
| 44 | | endom 9019 |
. . . . . 6
⊢ (dom
𝑂 ≈ 𝐴 → dom 𝑂 ≼ 𝐴) |
| 45 | | domwdom 9614 |
. . . . . 6
⊢ (dom
𝑂 ≼ 𝐴 → dom 𝑂 ≼* 𝐴) |
| 46 | 43, 44, 45 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐴) |
| 47 | | wdomtr 9615 |
. . . . 5
⊢ ((dom
𝑂 ≼* 𝐴 ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐵) |
| 48 | 46, 47 | sylancom 588 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐵) |
| 49 | | wdompwdom 9618 |
. . . 4
⊢ (dom
𝑂 ≼* 𝐵 → 𝒫 dom 𝑂 ≼ 𝒫 𝐵) |
| 50 | 48, 49 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝒫 dom 𝑂 ≼ 𝒫 𝐵) |
| 51 | | domtr 9047 |
. . 3
⊢ ((dom
𝑂 ≼ 𝒫 dom
𝑂 ∧ 𝒫 dom 𝑂 ≼ 𝒫 𝐵) → dom 𝑂 ≼ 𝒫 𝐵) |
| 52 | 29, 50, 51 | syl2anc 584 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼ 𝒫 𝐵) |
| 53 | | elharval 9601 |
. 2
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐵)
↔ (dom 𝑂 ∈ On
∧ dom 𝑂 ≼
𝒫 𝐵)) |
| 54 | 26, 52, 53 | sylanbrc 583 |
1
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ (har‘𝒫 𝐵)) |