Step | Hyp | Ref
| Expression |
1 | | isof1o 7269 |
. . . 4
β’ (πΉ Isom E , E (π΄, π΅) β πΉ:π΄β1-1-ontoβπ΅) |
2 | | f1of 6785 |
. . . 4
β’ (πΉ:π΄β1-1-ontoβπ΅ β πΉ:π΄βΆπ΅) |
3 | 1, 2 | syl 17 |
. . 3
β’ (πΉ Isom E , E (π΄, π΅) β πΉ:π΄βΆπ΅) |
4 | | ffdm 6699 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β (πΉ:dom πΉβΆπ΅ β§ dom πΉ β π΄)) |
5 | 4 | simpld 496 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β πΉ:dom πΉβΆπ΅) |
6 | | fss 6686 |
. . . . 5
β’ ((πΉ:dom πΉβΆπ΅ β§ π΅ β On) β πΉ:dom πΉβΆOn) |
7 | 5, 6 | sylan 581 |
. . . 4
β’ ((πΉ:π΄βΆπ΅ β§ π΅ β On) β πΉ:dom πΉβΆOn) |
8 | 7 | 3adant2 1132 |
. . 3
β’ ((πΉ:π΄βΆπ΅ β§ Ord π΄ β§ π΅ β On) β πΉ:dom πΉβΆOn) |
9 | 3, 8 | syl3an1 1164 |
. 2
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ π΅ β On) β πΉ:dom πΉβΆOn) |
10 | | fdm 6678 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β dom πΉ = π΄) |
11 | 10 | eqcomd 2739 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β π΄ = dom πΉ) |
12 | | ordeq 6325 |
. . . . 5
β’ (π΄ = dom πΉ β (Ord π΄ β Ord dom πΉ)) |
13 | 1, 2, 11, 12 | 4syl 19 |
. . . 4
β’ (πΉ Isom E , E (π΄, π΅) β (Ord π΄ β Ord dom πΉ)) |
14 | 13 | biimpa 478 |
. . 3
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄) β Ord dom πΉ) |
15 | 14 | 3adant3 1133 |
. 2
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ π΅ β On) β Ord dom πΉ) |
16 | 10 | eleq2d 2820 |
. . . . . . 7
β’ (πΉ:π΄βΆπ΅ β (π₯ β dom πΉ β π₯ β π΄)) |
17 | 10 | eleq2d 2820 |
. . . . . . 7
β’ (πΉ:π΄βΆπ΅ β (π¦ β dom πΉ β π¦ β π΄)) |
18 | 16, 17 | anbi12d 632 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β ((π₯ β dom πΉ β§ π¦ β dom πΉ) β (π₯ β π΄ β§ π¦ β π΄))) |
19 | 1, 2, 18 | 3syl 18 |
. . . . 5
β’ (πΉ Isom E , E (π΄, π΅) β ((π₯ β dom πΉ β§ π¦ β dom πΉ) β (π₯ β π΄ β§ π¦ β π΄))) |
20 | | isorel 7272 |
. . . . . . . 8
β’ ((πΉ Isom E , E (π΄, π΅) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ E π¦ β (πΉβπ₯) E (πΉβπ¦))) |
21 | | epel 5541 |
. . . . . . . 8
β’ (π₯ E π¦ β π₯ β π¦) |
22 | | fvex 6856 |
. . . . . . . . 9
β’ (πΉβπ¦) β V |
23 | 22 | epeli 5540 |
. . . . . . . 8
β’ ((πΉβπ₯) E (πΉβπ¦) β (πΉβπ₯) β (πΉβπ¦)) |
24 | 20, 21, 23 | 3bitr3g 313 |
. . . . . . 7
β’ ((πΉ Isom E , E (π΄, π΅) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦))) |
25 | 24 | biimpd 228 |
. . . . . 6
β’ ((πΉ Isom E , E (π΄, π΅) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦))) |
26 | 25 | ex 414 |
. . . . 5
β’ (πΉ Isom E , E (π΄, π΅) β ((π₯ β π΄ β§ π¦ β π΄) β (π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦)))) |
27 | 19, 26 | sylbid 239 |
. . . 4
β’ (πΉ Isom E , E (π΄, π΅) β ((π₯ β dom πΉ β§ π¦ β dom πΉ) β (π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦)))) |
28 | 27 | ralrimivv 3192 |
. . 3
β’ (πΉ Isom E , E (π΄, π΅) β βπ₯ β dom πΉβπ¦ β dom πΉ(π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦))) |
29 | 28 | 3ad2ant1 1134 |
. 2
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ π΅ β On) β βπ₯ β dom πΉβπ¦ β dom πΉ(π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦))) |
30 | | df-smo 8293 |
. 2
β’ (Smo
πΉ β (πΉ:dom πΉβΆOn β§ Ord dom πΉ β§ βπ₯ β dom πΉβπ¦ β dom πΉ(π₯ β π¦ β (πΉβπ₯) β (πΉβπ¦)))) |
31 | 9, 15, 29, 30 | syl3anbrc 1344 |
1
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ π΅ β On) β Smo πΉ) |