Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
β’ (π΄ = π΅ β π΄ = π΅) |
2 | | dmeq 5860 |
. . . 4
β’ (π΄ = π΅ β dom π΄ = dom π΅) |
3 | 1, 2 | feq12d 6657 |
. . 3
β’ (π΄ = π΅ β (π΄:dom π΄βΆOn β π΅:dom π΅βΆOn)) |
4 | | ordeq 6325 |
. . . 4
β’ (dom
π΄ = dom π΅ β (Ord dom π΄ β Ord dom π΅)) |
5 | 2, 4 | syl 17 |
. . 3
β’ (π΄ = π΅ β (Ord dom π΄ β Ord dom π΅)) |
6 | | fveq1 6842 |
. . . . . . 7
β’ (π΄ = π΅ β (π΄βπ₯) = (π΅βπ₯)) |
7 | | fveq1 6842 |
. . . . . . 7
β’ (π΄ = π΅ β (π΄βπ¦) = (π΅βπ¦)) |
8 | 6, 7 | eleq12d 2828 |
. . . . . 6
β’ (π΄ = π΅ β ((π΄βπ₯) β (π΄βπ¦) β (π΅βπ₯) β (π΅βπ¦))) |
9 | 8 | imbi2d 341 |
. . . . 5
β’ (π΄ = π΅ β ((π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β (π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
10 | 9 | 2ralbidv 3209 |
. . . 4
β’ (π΄ = π΅ β (βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
11 | 2 | raleqdv 3312 |
. . . . 5
β’ (π΄ = π΅ β (βπ¦ β dom π΄(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
12 | 11 | ralbidv 3171 |
. . . 4
β’ (π΄ = π΅ β (βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β βπ₯ β dom π΄βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
13 | 2 | raleqdv 3312 |
. . . 4
β’ (π΄ = π΅ β (βπ₯ β dom π΄βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)) β βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
14 | 10, 12, 13 | 3bitrd 305 |
. . 3
β’ (π΄ = π΅ β (βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)) β βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
15 | 3, 5, 14 | 3anbi123d 1437 |
. 2
β’ (π΄ = π΅ β ((π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦))) β (π΅:dom π΅βΆOn β§ Ord dom π΅ β§ βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦))))) |
16 | | df-smo 8293 |
. 2
β’ (Smo
π΄ β (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
17 | | df-smo 8293 |
. 2
β’ (Smo
π΅ β (π΅:dom π΅βΆOn β§ Ord dom π΅ β§ βπ₯ β dom π΅βπ¦ β dom π΅(π₯ β π¦ β (π΅βπ₯) β (π΅βπ¦)))) |
18 | 15, 16, 17 | 3bitr4g 314 |
1
β’ (π΄ = π΅ β (Smo π΄ β Smo π΅)) |