Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . 6
β’ dom π
= dom π
|
2 | 1 | ordthauslem 22894 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯π
π¦ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
3 | 1 | ordthauslem 22894 |
. . . . . . 7
β’ ((π
β TosetRel β§ π¦ β dom π
β§ π₯ β dom π
) β (π¦π
π₯ β (π¦ β π₯ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
)))) |
4 | | necom 2994 |
. . . . . . . 8
β’ (π¦ β π₯ β π₯ β π¦) |
5 | | 3ancoma 1098 |
. . . . . . . . . . 11
β’ ((π¦ β π β§ π₯ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
6 | | incom 4201 |
. . . . . . . . . . . . 13
β’ (π β© π) = (π β© π) |
7 | 6 | eqeq1i 2737 |
. . . . . . . . . . . 12
β’ ((π β© π) = β
β (π β© π) = β
) |
8 | 7 | 3anbi3i 1159 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
9 | 5, 8 | bitri 274 |
. . . . . . . . . 10
β’ ((π¦ β π β§ π₯ β π β§ (π β© π) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
10 | 9 | 2rexbii 3129 |
. . . . . . . . 9
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
11 | | rexcom 3287 |
. . . . . . . . 9
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
12 | 10, 11 | bitri 274 |
. . . . . . . 8
β’
(βπ β
(ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
13 | 4, 12 | imbi12i 350 |
. . . . . . 7
β’ ((π¦ β π₯ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π¦ β π β§ π₯ β π β§ (π β© π) = β
)) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
14 | 3, 13 | imbitrdi 250 |
. . . . . 6
β’ ((π
β TosetRel β§ π¦ β dom π
β§ π₯ β dom π
) β (π¦π
π₯ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
15 | 14 | 3com23 1126 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π¦π
π₯ β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
16 | 1 | tsrlin 18540 |
. . . . 5
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯π
π¦ β¨ π¦π
π₯)) |
17 | 2, 15, 16 | mpjaod 858 |
. . . 4
β’ ((π
β TosetRel β§ π₯ β dom π
β§ π¦ β dom π
) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
18 | 17 | 3expb 1120 |
. . 3
β’ ((π
β TosetRel β§ (π₯ β dom π
β§ π¦ β dom π
)) β (π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
19 | 18 | ralrimivva 3200 |
. 2
β’ (π
β TosetRel β
βπ₯ β dom π
βπ¦ β dom π
(π₯ β π¦ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
20 | 1 | ordttopon 22704 |
. . 3
β’ (π
β TosetRel β
(ordTopβπ
) β
(TopOnβdom π
)) |
21 | | ishaus2 22862 |
. . 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 256 |
1
β’ (π
β TosetRel β
(ordTopβπ
) β
Haus) |