Proof of Theorem hsmexlem1
Step | Hyp | Ref
| Expression |
1 | | hsmexlem.o |
. . . 4
⊢ 𝑂 = OrdIso( E , 𝐴) |
2 | 1 | oicl 8434 |
. . 3
⊢ Ord dom
𝑂 |
3 | | relwdom 8471 |
. . . . . . . 8
⊢ Rel
≼* |
4 | 3 | brrelexi 5158 |
. . . . . . 7
⊢ (𝐴 ≼* 𝐵 → 𝐴 ∈ V) |
5 | 4 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ∈ V) |
6 | | uniexg 6955 |
. . . . . 6
⊢ (𝐴 ∈ V → ∪ 𝐴
∈ V) |
7 | | sucexg 7010 |
. . . . . 6
⊢ (∪ 𝐴
∈ V → suc ∪ 𝐴 ∈ V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → suc ∪ 𝐴
∈ V) |
9 | 1 | oif 8435 |
. . . . . . 7
⊢ 𝑂:dom 𝑂⟶𝐴 |
10 | | onsucuni 7028 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ⊆ suc ∪
𝐴) |
12 | | fss 6056 |
. . . . . . 7
⊢ ((𝑂:dom 𝑂⟶𝐴 ∧ 𝐴 ⊆ suc ∪
𝐴) → 𝑂:dom 𝑂⟶suc ∪
𝐴) |
13 | 9, 11, 12 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂:dom 𝑂⟶suc ∪
𝐴) |
14 | 1 | oismo 8445 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → (Smo 𝑂 ∧ ran 𝑂 = 𝐴)) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (Smo 𝑂 ∧ ran 𝑂 = 𝐴)) |
16 | 15 | simpld 475 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Smo 𝑂) |
17 | | ssorduni 6985 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
18 | 17 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Ord ∪ 𝐴) |
19 | | ordsuc 7014 |
. . . . . . 7
⊢ (Ord
∪ 𝐴 ↔ Ord suc ∪
𝐴) |
20 | 18, 19 | sylib 208 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → Ord suc ∪ 𝐴) |
21 | | smorndom 7465 |
. . . . . 6
⊢ ((𝑂:dom 𝑂⟶suc ∪
𝐴 ∧ Smo 𝑂 ∧ Ord suc ∪ 𝐴)
→ dom 𝑂 ⊆ suc
∪ 𝐴) |
22 | 13, 16, 20, 21 | syl3anc 1326 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ⊆ suc ∪
𝐴) |
23 | 8, 22 | ssexd 4805 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ V) |
24 | | elong 5731 |
. . . 4
⊢ (dom
𝑂 ∈ V → (dom
𝑂 ∈ On ↔ Ord dom
𝑂)) |
25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (dom 𝑂 ∈ On ↔ Ord dom 𝑂)) |
26 | 2, 25 | mpbiri 248 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ On) |
27 | | canth2g 8114 |
. . . 4
⊢ (dom
𝑂 ∈ V → dom 𝑂 ≺ 𝒫 dom 𝑂) |
28 | | sdomdom 7983 |
. . . 4
⊢ (dom
𝑂 ≺ 𝒫 dom
𝑂 → dom 𝑂 ≼ 𝒫 dom 𝑂) |
29 | 23, 27, 28 | 3syl 18 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼ 𝒫 dom 𝑂) |
30 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝐴 ⊆ On) |
31 | | epweon 6983 |
. . . . . . . . . . 11
⊢ E We
On |
32 | | wess 5101 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ On → ( E We On
→ E We 𝐴)) |
33 | 30, 31, 32 | mpisyl 21 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → E We 𝐴) |
34 | | epse 5097 |
. . . . . . . . . 10
⊢ E Se
𝐴 |
35 | 1 | oiiso2 8436 |
. . . . . . . . . 10
⊢ (( E We
𝐴 ∧ E Se 𝐴) → 𝑂 Isom E , E (dom 𝑂, ran 𝑂)) |
36 | 33, 34, 35 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂 Isom E , E (dom 𝑂, ran 𝑂)) |
37 | | isof1o 6573 |
. . . . . . . . 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 479 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → ran 𝑂 = 𝐴) |
40 | | f1oeq3 6129 |
. . . . . . . . 9
⊢ (ran
𝑂 = 𝐴 → (𝑂:dom 𝑂–1-1-onto→ran
𝑂 ↔ 𝑂:dom 𝑂–1-1-onto→𝐴)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → (𝑂:dom 𝑂–1-1-onto→ran
𝑂 ↔ 𝑂:dom 𝑂–1-1-onto→𝐴)) |
42 | 38, 41 | mpbid 222 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝑂:dom 𝑂–1-1-onto→𝐴) |
43 | | f1oen2g 7972 |
. . . . . . 7
⊢ ((dom
𝑂 ∈ On ∧ 𝐴 ∈ V ∧ 𝑂:dom 𝑂–1-1-onto→𝐴) → dom 𝑂 ≈ 𝐴) |
44 | 26, 5, 42, 43 | syl3anc 1326 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≈ 𝐴) |
45 | | endom 7982 |
. . . . . 6
⊢ (dom
𝑂 ≈ 𝐴 → dom 𝑂 ≼ 𝐴) |
46 | | domwdom 8479 |
. . . . . 6
⊢ (dom
𝑂 ≼ 𝐴 → dom 𝑂 ≼* 𝐴) |
47 | 44, 45, 46 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐴) |
48 | | wdomtr 8480 |
. . . . 5
⊢ ((dom
𝑂 ≼* 𝐴 ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐵) |
49 | 47, 48 | sylancom 701 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼* 𝐵) |
50 | | wdompwdom 8483 |
. . . 4
⊢ (dom
𝑂 ≼* 𝐵 → 𝒫 dom 𝑂 ≼ 𝒫 𝐵) |
51 | 49, 50 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → 𝒫 dom 𝑂 ≼ 𝒫 𝐵) |
52 | | domtr 8009 |
. . 3
⊢ ((dom
𝑂 ≼ 𝒫 dom
𝑂 ∧ 𝒫 dom 𝑂 ≼ 𝒫 𝐵) → dom 𝑂 ≼ 𝒫 𝐵) |
53 | 29, 51, 52 | syl2anc 693 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ≼ 𝒫 𝐵) |
54 | | elharval 8468 |
. 2
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐵)
↔ (dom 𝑂 ∈ On
∧ dom 𝑂 ≼
𝒫 𝐵)) |
55 | 26, 53, 54 | sylanbrc 698 |
1
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ (har‘𝒫 𝐵)) |