Step | Hyp | Ref
| Expression |
1 | | hsmexlem.o |
. . . 4
β’ π = OrdIso( E , π΄) |
2 | 1 | oicl 9526 |
. . 3
β’ Ord dom
π |
3 | | relwdom 9563 |
. . . . . . . 8
β’ Rel
βΌ* |
4 | 3 | brrelex1i 5732 |
. . . . . . 7
β’ (π΄ βΌ* π΅ β π΄ β V) |
5 | 4 | adantl 482 |
. . . . . 6
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π΄ β V) |
6 | | uniexg 7732 |
. . . . . 6
β’ (π΄ β V β βͺ π΄
β V) |
7 | | sucexg 7795 |
. . . . . 6
β’ (βͺ π΄
β V β suc βͺ π΄ β V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
β’ ((π΄ β On β§ π΄ βΌ* π΅) β suc βͺ π΄
β V) |
9 | 1 | oif 9527 |
. . . . . . 7
β’ π:dom πβΆπ΄ |
10 | | onsucuni 7818 |
. . . . . . . 8
β’ (π΄ β On β π΄ β suc βͺ π΄) |
11 | 10 | adantr 481 |
. . . . . . 7
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π΄ β suc βͺ
π΄) |
12 | | fss 6734 |
. . . . . . 7
β’ ((π:dom πβΆπ΄ β§ π΄ β suc βͺ
π΄) β π:dom πβΆsuc βͺ
π΄) |
13 | 9, 11, 12 | sylancr 587 |
. . . . . 6
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π:dom πβΆsuc βͺ
π΄) |
14 | 1 | oismo 9537 |
. . . . . . . 8
β’ (π΄ β On β (Smo π β§ ran π = π΄)) |
15 | 14 | adantr 481 |
. . . . . . 7
β’ ((π΄ β On β§ π΄ βΌ* π΅) β (Smo π β§ ran π = π΄)) |
16 | 15 | simpld 495 |
. . . . . 6
β’ ((π΄ β On β§ π΄ βΌ* π΅) β Smo π) |
17 | | ssorduni 7768 |
. . . . . . . 8
β’ (π΄ β On β Ord βͺ π΄) |
18 | 17 | adantr 481 |
. . . . . . 7
β’ ((π΄ β On β§ π΄ βΌ* π΅) β Ord βͺ π΄) |
19 | | ordsuc 7803 |
. . . . . . 7
β’ (Ord
βͺ π΄ β Ord suc βͺ
π΄) |
20 | 18, 19 | sylib 217 |
. . . . . 6
β’ ((π΄ β On β§ π΄ βΌ* π΅) β Ord suc βͺ π΄) |
21 | | smocdmdom 8370 |
. . . . . 6
β’ ((π:dom πβΆsuc βͺ
π΄ β§ Smo π β§ Ord suc βͺ π΄)
β dom π β suc
βͺ π΄) |
22 | 13, 16, 20, 21 | syl3anc 1371 |
. . . . 5
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π β suc βͺ
π΄) |
23 | 8, 22 | ssexd 5324 |
. . . 4
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π β V) |
24 | | elong 6372 |
. . . 4
β’ (dom
π β V β (dom
π β On β Ord dom
π)) |
25 | 23, 24 | syl 17 |
. . 3
β’ ((π΄ β On β§ π΄ βΌ* π΅) β (dom π β On β Ord dom π)) |
26 | 2, 25 | mpbiri 257 |
. 2
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π β On) |
27 | | canth2g 9133 |
. . . 4
β’ (dom
π β V β dom π βΊ π« dom π) |
28 | | sdomdom 8978 |
. . . 4
β’ (dom
π βΊ π« dom
π β dom π βΌ π« dom π) |
29 | 23, 27, 28 | 3syl 18 |
. . 3
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π βΌ π« dom π) |
30 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π΄ β On) |
31 | | epweon 7764 |
. . . . . . . . . . 11
β’ E We
On |
32 | | wess 5663 |
. . . . . . . . . . 11
β’ (π΄ β On β ( E We On
β E We π΄)) |
33 | 30, 31, 32 | mpisyl 21 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΄ βΌ* π΅) β E We π΄) |
34 | | epse 5659 |
. . . . . . . . . 10
β’ E Se
π΄ |
35 | 1 | oiiso2 9528 |
. . . . . . . . . 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 7322 |
. . . . . . . . 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 496 |
. . . . . . . . 9
β’ ((π΄ β On β§ π΄ βΌ* π΅) β ran π = π΄) |
40 | 39 | f1oeq3d 6830 |
. . . . . . . 8
β’ ((π΄ β On β§ π΄ βΌ* π΅) β (π:dom πβ1-1-ontoβran
π β π:dom πβ1-1-ontoβπ΄)) |
41 | 38, 40 | mpbid 231 |
. . . . . . 7
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π:dom πβ1-1-ontoβπ΄) |
42 | | f1oen2g 8966 |
. . . . . . 7
β’ ((dom
π β On β§ π΄ β V β§ π:dom πβ1-1-ontoβπ΄) β dom π β π΄) |
43 | 26, 5, 41, 42 | syl3anc 1371 |
. . . . . 6
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π β π΄) |
44 | | endom 8977 |
. . . . . 6
β’ (dom
π β π΄ β dom π βΌ π΄) |
45 | | domwdom 9571 |
. . . . . 6
β’ (dom
π βΌ π΄ β dom π βΌ* π΄) |
46 | 43, 44, 45 | 3syl 18 |
. . . . 5
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π βΌ* π΄) |
47 | | wdomtr 9572 |
. . . . 5
β’ ((dom
π βΌ* π΄ β§ π΄ βΌ* π΅) β dom π βΌ* π΅) |
48 | 46, 47 | sylancom 588 |
. . . 4
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π βΌ* π΅) |
49 | | wdompwdom 9575 |
. . . 4
β’ (dom
π βΌ* π΅ β π« dom π βΌ π« π΅) |
50 | 48, 49 | syl 17 |
. . 3
β’ ((π΄ β On β§ π΄ βΌ* π΅) β π« dom π βΌ π« π΅) |
51 | | domtr 9005 |
. . 3
β’ ((dom
π βΌ π« dom
π β§ π« dom π βΌ π« π΅) β dom π βΌ π« π΅) |
52 | 29, 50, 51 | syl2anc 584 |
. 2
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π βΌ π« π΅) |
53 | | elharval 9558 |
. 2
β’ (dom
π β
(harβπ« π΅)
β (dom π β On
β§ dom π βΌ
π« π΅)) |
54 | 26, 52, 53 | sylanbrc 583 |
1
β’ ((π΄ β On β§ π΄ βΌ* π΅) β dom π β (harβπ« π΅)) |