Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’ dom π
= dom π
|
2 | 1 | ordthauslem 22750 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯π
π¦ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
3 | 1 | ordthauslem 22750 |
. . . . . . 7
β’ ((π
β TosetRel β§ π¦ β dom π
β§ π₯ β dom π
) β (π¦π
π₯ β (π¦ β π₯ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
)))) |
4 | | necom 2994 |
. . . . . . . 8
β’ (π¦ β π₯ β π₯ β π¦) |
5 | | 3ancoma 1099 |
. . . . . . . . . . 11
β’ ((π¦ β π β§ π₯ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
6 | | incom 4162 |
. . . . . . . . . . . . 13
β’ (π β© π) = (π β© π) |
7 | 6 | eqeq1i 2738 |
. . . . . . . . . . . 12
β’ ((π β© π) = β
β (π β© π) = β
) |
8 | 7 | 3anbi3i 1160 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
9 | 5, 8 | bitri 275 |
. . . . . . . . . 10
β’ ((π¦ β π β§ π₯ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
10 | 9 | 2rexbii 3125 |
. . . . . . . . 9
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
11 | | rexcom 3272 |
. . . . . . . . 9
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
12 | 10, 11 | bitri 275 |
. . . . . . . 8
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
13 | 4, 12 | imbi12i 351 |
. . . . . . 7
β’ ((π¦ β π₯ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
)) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
14 | 3, 13 | syl6ib 251 |
. . . . . 6
β’ ((π
β TosetRel β§ π¦ β dom π
β§ π₯ β dom π
) β (π¦π
π₯ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
15 | 14 | 3com23 1127 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π¦π
π₯ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
16 | 1 | tsrlin 18479 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯π
π¦ β¨ π¦π
π₯)) |
17 | 2, 15, 16 | mpjaod 859 |
. . . 4
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
18 | 17 | 3expb 1121 |
. . 3
β’ ((π
β TosetRel β§ (π₯ β dom π
β§ π¦ β dom π
)) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
19 | 18 | ralrimivva 3194 |
. 2
β’ (π
β TosetRel β
βπ₯ β dom π
βπ¦ β dom π
(π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
20 | 1 | ordttopon 22560 |
. . 3
β’ (π
β TosetRel β
(ordTopβπ
) β
(TopOnβdom π
)) |
21 | | ishaus2 22718 |
. . 3
β’
((ordTopβπ
)
β (TopOnβdom π
)
β ((ordTopβπ
)
β Haus β βπ₯ β dom π
βπ¦ β dom π
(π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
22 | 20, 21 | syl 17 |
. 2
β’ (π
β TosetRel β
((ordTopβπ
) β
Haus β βπ₯
β dom π
βπ¦ β dom π
(π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
23 | 19, 22 | mpbird 257 |
1
β’ (π
β TosetRel β
(ordTopβπ
) β
Haus) |