Step | Hyp | Ref
| Expression |
1 | | simpll1 1213 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β π
β TosetRel ) |
2 | | simpll3 1215 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β π΅ β π) |
3 | | ordthauslem.1 |
. . . . . . 7
β’ π = dom π
|
4 | 3 | ordtopn2 22562 |
. . . . . 6
β’ ((π
β TosetRel β§ π΅ β π) β {π₯ β π β£ Β¬ π΅π
π₯} β (ordTopβπ
)) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β {π₯ β π β£ Β¬ π΅π
π₯} β (ordTopβπ
)) |
6 | | simpll2 1214 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β π΄ β π) |
7 | 3 | ordtopn1 22561 |
. . . . . 6
β’ ((π
β TosetRel β§ π΄ β π) β {π₯ β π β£ Β¬ π₯π
π΄} β (ordTopβπ
)) |
8 | 1, 6, 7 | syl2anc 585 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β {π₯ β π β£ Β¬ π₯π
π΄} β (ordTopβπ
)) |
9 | | breq2 5114 |
. . . . . . 7
β’ (π₯ = π΄ β (π΅π
π₯ β π΅π
π΄)) |
10 | 9 | notbid 318 |
. . . . . 6
β’ (π₯ = π΄ β (Β¬ π΅π
π₯ β Β¬ π΅π
π΄)) |
11 | | simprr 772 |
. . . . . . . 8
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β π΄ β π΅) |
12 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β π
β TosetRel ) |
13 | | tsrps 18483 |
. . . . . . . . . . 11
β’ (π
β TosetRel β π
β
PosetRel) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β π
β PosetRel) |
15 | | simprl 770 |
. . . . . . . . . 10
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β π΄π
π΅) |
16 | | psasym 18472 |
. . . . . . . . . . 11
β’ ((π
β PosetRel β§ π΄π
π΅ β§ π΅π
π΄) β π΄ = π΅) |
17 | 16 | 3expia 1122 |
. . . . . . . . . 10
β’ ((π
β PosetRel β§ π΄π
π΅) β (π΅π
π΄ β π΄ = π΅)) |
18 | 14, 15, 17 | syl2anc 585 |
. . . . . . . . 9
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β (π΅π
π΄ β π΄ = π΅)) |
19 | 18 | necon3ad 2957 |
. . . . . . . 8
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β (π΄ β π΅ β Β¬ π΅π
π΄)) |
20 | 11, 19 | mpd 15 |
. . . . . . 7
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β Β¬ π΅π
π΄) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β Β¬ π΅π
π΄) |
22 | 10, 6, 21 | elrabd 3652 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β π΄ β {π₯ β π β£ Β¬ π΅π
π₯}) |
23 | | breq1 5113 |
. . . . . . 7
β’ (π₯ = π΅ β (π₯π
π΄ β π΅π
π΄)) |
24 | 23 | notbid 318 |
. . . . . 6
β’ (π₯ = π΅ β (Β¬ π₯π
π΄ β Β¬ π΅π
π΄)) |
25 | 24, 2, 21 | elrabd 3652 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β π΅ β {π₯ β π β£ Β¬ π₯π
π΄}) |
26 | | simpr 486 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) |
27 | | eleq2 2827 |
. . . . . . 7
β’ (π = {π₯ β π β£ Β¬ π΅π
π₯} β (π΄ β π β π΄ β {π₯ β π β£ Β¬ π΅π
π₯})) |
28 | | ineq1 4170 |
. . . . . . . 8
β’ (π = {π₯ β π β£ Β¬ π΅π
π₯} β (π β© π) = ({π₯ β π β£ Β¬ π΅π
π₯} β© π)) |
29 | 28 | eqeq1d 2739 |
. . . . . . 7
β’ (π = {π₯ β π β£ Β¬ π΅π
π₯} β ((π β© π) = β
β ({π₯ β π β£ Β¬ π΅π
π₯} β© π) = β
)) |
30 | 27, 29 | 3anbi13d 1439 |
. . . . . 6
β’ (π = {π₯ β π β£ Β¬ π΅π
π₯} β ((π΄ β π β§ π΅ β π β§ (π β© π) = β
) β (π΄ β {π₯ β π β£ Β¬ π΅π
π₯} β§ π΅ β π β§ ({π₯ β π β£ Β¬ π΅π
π₯} β© π) = β
))) |
31 | | eleq2 2827 |
. . . . . . 7
β’ (π = {π₯ β π β£ Β¬ π₯π
π΄} β (π΅ β π β π΅ β {π₯ β π β£ Β¬ π₯π
π΄})) |
32 | | ineq2 4171 |
. . . . . . . . 9
β’ (π = {π₯ β π β£ Β¬ π₯π
π΄} β ({π₯ β π β£ Β¬ π΅π
π₯} β© π) = ({π₯ β π β£ Β¬ π΅π
π₯} β© {π₯ β π β£ Β¬ π₯π
π΄})) |
33 | | inrab 4271 |
. . . . . . . . 9
β’ ({π₯ β π β£ Β¬ π΅π
π₯} β© {π₯ β π β£ Β¬ π₯π
π΄}) = {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} |
34 | 32, 33 | eqtrdi 2793 |
. . . . . . . 8
β’ (π = {π₯ β π β£ Β¬ π₯π
π΄} β ({π₯ β π β£ Β¬ π΅π
π₯} β© π) = {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)}) |
35 | 34 | eqeq1d 2739 |
. . . . . . 7
β’ (π = {π₯ β π β£ Β¬ π₯π
π΄} β (({π₯ β π β£ Β¬ π΅π
π₯} β© π) = β
β {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
)) |
36 | 31, 35 | 3anbi23d 1440 |
. . . . . 6
β’ (π = {π₯ β π β£ Β¬ π₯π
π΄} β ((π΄ β {π₯ β π β£ Β¬ π΅π
π₯} β§ π΅ β π β§ ({π₯ β π β£ Β¬ π΅π
π₯} β© π) = β
) β (π΄ β {π₯ β π β£ Β¬ π΅π
π₯} β§ π΅ β {π₯ β π β£ Β¬ π₯π
π΄} β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
))) |
37 | 30, 36 | rspc2ev 3595 |
. . . . 5
β’ (({π₯ β π β£ Β¬ π΅π
π₯} β (ordTopβπ
) β§ {π₯ β π β£ Β¬ π₯π
π΄} β (ordTopβπ
) β§ (π΄ β {π₯ β π β£ Β¬ π΅π
π₯} β§ π΅ β {π₯ β π β£ Β¬ π₯π
π΄} β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
)) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)) |
38 | 5, 8, 22, 25, 26, 37 | syl113anc 1383 |
. . . 4
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ {π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)) |
39 | 38 | ex 414 |
. . 3
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β ({π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} = β
β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
))) |
40 | | rabn0 4350 |
. . . 4
β’ ({π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} β β
β βπ₯ β π (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)) |
41 | | simpll1 1213 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π
β TosetRel ) |
42 | | simprl 770 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π₯ β π) |
43 | 3 | ordtopn2 22562 |
. . . . . . 7
β’ ((π
β TosetRel β§ π₯ β π) β {π¦ β π β£ Β¬ π₯π
π¦} β (ordTopβπ
)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β {π¦ β π β£ Β¬ π₯π
π¦} β (ordTopβπ
)) |
45 | 3 | ordtopn1 22561 |
. . . . . . 7
β’ ((π
β TosetRel β§ π₯ β π) β {π¦ β π β£ Β¬ π¦π
π₯} β (ordTopβπ
)) |
46 | 41, 42, 45 | syl2anc 585 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β {π¦ β π β£ Β¬ π¦π
π₯} β (ordTopβπ
)) |
47 | | breq2 5114 |
. . . . . . . 8
β’ (π¦ = π΄ β (π₯π
π¦ β π₯π
π΄)) |
48 | 47 | notbid 318 |
. . . . . . 7
β’ (π¦ = π΄ β (Β¬ π₯π
π¦ β Β¬ π₯π
π΄)) |
49 | | simpll2 1214 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π΄ β π) |
50 | | simprrr 781 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β Β¬ π₯π
π΄) |
51 | 48, 49, 50 | elrabd 3652 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π΄ β {π¦ β π β£ Β¬ π₯π
π¦}) |
52 | | breq1 5113 |
. . . . . . . 8
β’ (π¦ = π΅ β (π¦π
π₯ β π΅π
π₯)) |
53 | 52 | notbid 318 |
. . . . . . 7
β’ (π¦ = π΅ β (Β¬ π¦π
π₯ β Β¬ π΅π
π₯)) |
54 | | simpll3 1215 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π΅ β π) |
55 | | simprrl 780 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β Β¬ π΅π
π₯) |
56 | 53, 54, 55 | elrabd 3652 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β π΅ β {π¦ β π β£ Β¬ π¦π
π₯}) |
57 | 41, 42 | jca 513 |
. . . . . . . . . 10
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β (π
β TosetRel β§ π₯ β π)) |
58 | 3 | tsrlin 18481 |
. . . . . . . . . . 11
β’ ((π
β TosetRel β§ π₯ β π β§ π¦ β π) β (π₯π
π¦ β¨ π¦π
π₯)) |
59 | 58 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π
β TosetRel β§ π₯ β π) β§ π¦ β π) β (π₯π
π¦ β¨ π¦π
π₯)) |
60 | 57, 59 | sylan 581 |
. . . . . . . . 9
β’
(((((π
β
TosetRel β§ π΄ β
π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β§ π¦ β π) β (π₯π
π¦ β¨ π¦π
π₯)) |
61 | | oran 989 |
. . . . . . . . 9
β’ ((π₯π
π¦ β¨ π¦π
π₯) β Β¬ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)) |
62 | 60, 61 | sylib 217 |
. . . . . . . 8
β’
(((((π
β
TosetRel β§ π΄ β
π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β§ π¦ β π) β Β¬ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)) |
63 | 62 | ralrimiva 3144 |
. . . . . . 7
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β βπ¦ β π Β¬ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)) |
64 | | rabeq0 4349 |
. . . . . . 7
β’ ({π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} = β
β βπ¦ β π Β¬ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)) |
65 | 63, 64 | sylibr 233 |
. . . . . 6
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} = β
) |
66 | | eleq2 2827 |
. . . . . . . 8
β’ (π = {π¦ β π β£ Β¬ π₯π
π¦} β (π΄ β π β π΄ β {π¦ β π β£ Β¬ π₯π
π¦})) |
67 | | ineq1 4170 |
. . . . . . . . 9
β’ (π = {π¦ β π β£ Β¬ π₯π
π¦} β (π β© π) = ({π¦ β π β£ Β¬ π₯π
π¦} β© π)) |
68 | 67 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = {π¦ β π β£ Β¬ π₯π
π¦} β ((π β© π) = β
β ({π¦ β π β£ Β¬ π₯π
π¦} β© π) = β
)) |
69 | 66, 68 | 3anbi13d 1439 |
. . . . . . 7
β’ (π = {π¦ β π β£ Β¬ π₯π
π¦} β ((π΄ β π β§ π΅ β π β§ (π β© π) = β
) β (π΄ β {π¦ β π β£ Β¬ π₯π
π¦} β§ π΅ β π β§ ({π¦ β π β£ Β¬ π₯π
π¦} β© π) = β
))) |
70 | | eleq2 2827 |
. . . . . . . 8
β’ (π = {π¦ β π β£ Β¬ π¦π
π₯} β (π΅ β π β π΅ β {π¦ β π β£ Β¬ π¦π
π₯})) |
71 | | ineq2 4171 |
. . . . . . . . . 10
β’ (π = {π¦ β π β£ Β¬ π¦π
π₯} β ({π¦ β π β£ Β¬ π₯π
π¦} β© π) = ({π¦ β π β£ Β¬ π₯π
π¦} β© {π¦ β π β£ Β¬ π¦π
π₯})) |
72 | | inrab 4271 |
. . . . . . . . . 10
β’ ({π¦ β π β£ Β¬ π₯π
π¦} β© {π¦ β π β£ Β¬ π¦π
π₯}) = {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} |
73 | 71, 72 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π = {π¦ β π β£ Β¬ π¦π
π₯} β ({π¦ β π β£ Β¬ π₯π
π¦} β© π) = {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)}) |
74 | 73 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = {π¦ β π β£ Β¬ π¦π
π₯} β (({π¦ β π β£ Β¬ π₯π
π¦} β© π) = β
β {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} = β
)) |
75 | 70, 74 | 3anbi23d 1440 |
. . . . . . 7
β’ (π = {π¦ β π β£ Β¬ π¦π
π₯} β ((π΄ β {π¦ β π β£ Β¬ π₯π
π¦} β§ π΅ β π β§ ({π¦ β π β£ Β¬ π₯π
π¦} β© π) = β
) β (π΄ β {π¦ β π β£ Β¬ π₯π
π¦} β§ π΅ β {π¦ β π β£ Β¬ π¦π
π₯} β§ {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} = β
))) |
76 | 69, 75 | rspc2ev 3595 |
. . . . . 6
β’ (({π¦ β π β£ Β¬ π₯π
π¦} β (ordTopβπ
) β§ {π¦ β π β£ Β¬ π¦π
π₯} β (ordTopβπ
) β§ (π΄ β {π¦ β π β£ Β¬ π₯π
π¦} β§ π΅ β {π¦ β π β£ Β¬ π¦π
π₯} β§ {π¦ β π β£ (Β¬ π₯π
π¦ β§ Β¬ π¦π
π₯)} = β
)) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)) |
77 | 44, 46, 51, 56, 65, 76 | syl113anc 1383 |
. . . . 5
β’ ((((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β§ (π₯ β π β§ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄))) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)) |
78 | 77 | rexlimdvaa 3154 |
. . . 4
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β (βπ₯ β π (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
))) |
79 | 40, 78 | biimtrid 241 |
. . 3
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β ({π₯ β π β£ (Β¬ π΅π
π₯ β§ Β¬ π₯π
π΄)} β β
β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
))) |
80 | 39, 79 | pm2.61dne 3032 |
. 2
β’ (((π
β TosetRel β§ π΄ β π β§ π΅ β π) β§ (π΄π
π΅ β§ π΄ β π΅)) β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)) |
81 | 80 | exp32 422 |
1
β’ ((π
β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π
π΅ β (π΄ β π΅ β βπ β (ordTopβπ
)βπ β (ordTopβπ
)(π΄ β π β§ π΅ β π β§ (π β© π) = β
)))) |