Step | Hyp | Ref
| Expression |
1 | | ordtrest2.2 |
. . . 4
β’ (π β π
β TosetRel ) |
2 | | tsrps 18481 |
. . . 4
β’ (π
β TosetRel β π
β
PosetRel) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π
β PosetRel) |
4 | | ordtrest2.1 |
. . . . 5
β’ π = dom π
|
5 | 1 | dmexd 7843 |
. . . . 5
β’ (π β dom π
β V) |
6 | 4, 5 | eqeltrid 2838 |
. . . 4
β’ (π β π β V) |
7 | | ordtrest2.3 |
. . . 4
β’ (π β π΄ β π) |
8 | 6, 7 | ssexd 5282 |
. . 3
β’ (π β π΄ β V) |
9 | | ordtrest 22569 |
. . 3
β’ ((π
β PosetRel β§ π΄ β V) β
(ordTopβ(π
β©
(π΄ Γ π΄))) β ((ordTopβπ
) βΎt π΄)) |
10 | 3, 8, 9 | syl2anc 585 |
. 2
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) β ((ordTopβπ
) βΎt π΄)) |
11 | | eqid 2733 |
. . . . . . . 8
β’ ran
(π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) = ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) |
12 | | eqid 2733 |
. . . . . . . 8
β’ ran
(π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}) = ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}) |
13 | 4, 11, 12 | ordtval 22556 |
. . . . . . 7
β’ (π
β TosetRel β
(ordTopβπ
) =
(topGenβ(fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))))) |
14 | 1, 13 | syl 17 |
. . . . . 6
β’ (π β (ordTopβπ
) =
(topGenβ(fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))))) |
15 | 14 | oveq1d 7373 |
. . . . 5
β’ (π β ((ordTopβπ
) βΎt π΄) =
((topGenβ(fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))))) βΎt π΄)) |
16 | | fibas 22343 |
. . . . . 6
β’
(fiβ({π} βͺ
(ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) β TopBases |
17 | | tgrest 22526 |
. . . . . 6
β’
(((fiβ({π}
βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) β TopBases β§ π΄ β V) β
(topGenβ((fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) βΎt π΄)) = ((topGenβ(fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))))) βΎt π΄)) |
18 | 16, 8, 17 | sylancr 588 |
. . . . 5
β’ (π β
(topGenβ((fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) βΎt π΄)) = ((topGenβ(fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))))) βΎt π΄)) |
19 | 15, 18 | eqtr4d 2776 |
. . . 4
β’ (π β ((ordTopβπ
) βΎt π΄) =
(topGenβ((fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) βΎt π΄))) |
20 | | firest 17319 |
. . . . 5
β’
(fiβ(({π}
βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄)) = ((fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) βΎt π΄) |
21 | 20 | fveq2i 6846 |
. . . 4
β’
(topGenβ(fiβ(({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄))) = (topGenβ((fiβ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) βΎt π΄)) |
22 | 19, 21 | eqtr4di 2791 |
. . 3
β’ (π β ((ordTopβπ
) βΎt π΄) =
(topGenβ(fiβ(({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄)))) |
23 | | inex1g 5277 |
. . . . . 6
β’ (π
β TosetRel β (π
β© (π΄ Γ π΄)) β V) |
24 | 1, 23 | syl 17 |
. . . . 5
β’ (π β (π
β© (π΄ Γ π΄)) β V) |
25 | | ordttop 22567 |
. . . . 5
β’ ((π
β© (π΄ Γ π΄)) β V β (ordTopβ(π
β© (π΄ Γ π΄))) β Top) |
26 | 24, 25 | syl 17 |
. . . 4
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) β Top) |
27 | 4, 11, 12 | ordtuni 22557 |
. . . . . . . . 9
β’ (π
β TosetRel β π = βͺ
({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) |
28 | 1, 27 | syl 17 |
. . . . . . . 8
β’ (π β π = βͺ ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))) |
29 | 28, 6 | eqeltrrd 2835 |
. . . . . . 7
β’ (π β βͺ ({π}
βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β V) |
30 | | uniexb 7699 |
. . . . . . 7
β’ (({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β V β βͺ ({π}
βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β V) |
31 | 29, 30 | sylibr 233 |
. . . . . 6
β’ (π β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β V) |
32 | | restval 17313 |
. . . . . 6
β’ ((({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β V β§ π΄ β V) β (({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄) = ran (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄))) |
33 | 31, 8, 32 | syl2anc 585 |
. . . . 5
β’ (π β (({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄) = ran (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄))) |
34 | | sseqin2 4176 |
. . . . . . . . . . . 12
β’ (π΄ β π β (π β© π΄) = π΄) |
35 | 7, 34 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π β© π΄) = π΄) |
36 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ dom
(π
β© (π΄ Γ π΄)) = dom (π
β© (π΄ Γ π΄)) |
37 | 36 | ordttopon 22560 |
. . . . . . . . . . . . . 14
β’ ((π
β© (π΄ Γ π΄)) β V β (ordTopβ(π
β© (π΄ Γ π΄))) β (TopOnβdom (π
β© (π΄ Γ π΄)))) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) β (TopOnβdom (π
β© (π΄ Γ π΄)))) |
39 | 4 | psssdm 18476 |
. . . . . . . . . . . . . . 15
β’ ((π
β PosetRel β§ π΄ β π) β dom (π
β© (π΄ Γ π΄)) = π΄) |
40 | 3, 7, 39 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β dom (π
β© (π΄ Γ π΄)) = π΄) |
41 | 40 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π β (TopOnβdom (π
β© (π΄ Γ π΄))) = (TopOnβπ΄)) |
42 | 38, 41 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) β (TopOnβπ΄)) |
43 | | toponmax 22291 |
. . . . . . . . . . . 12
β’
((ordTopβ(π
β© (π΄ Γ π΄))) β (TopOnβπ΄) β π΄ β (ordTopβ(π
β© (π΄ Γ π΄)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
β’ (π β π΄ β (ordTopβ(π
β© (π΄ Γ π΄)))) |
45 | 35, 44 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π β (π β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
46 | | elsni 4604 |
. . . . . . . . . . . 12
β’ (π£ β {π} β π£ = π) |
47 | 46 | ineq1d 4172 |
. . . . . . . . . . 11
β’ (π£ β {π} β (π£ β© π΄) = (π β© π΄)) |
48 | 47 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π£ β {π} β ((π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β (π β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))))) |
49 | 45, 48 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (π β (π£ β {π} β (π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))))) |
50 | 49 | ralrimiv 3139 |
. . . . . . . 8
β’ (π β βπ£ β {π} (π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
51 | | ordtrest2.4 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π
π§ β§ π§π
π¦)} β π΄) |
52 | 4, 1, 7, 51 | ordtrest2lem 22570 |
. . . . . . . . 9
β’ (π β βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§})(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
53 | | df-rn 5645 |
. . . . . . . . . . 11
β’ ran π
= dom β‘π
|
54 | | cnvtsr 18482 |
. . . . . . . . . . . 12
β’ (π
β TosetRel β β‘π
β TosetRel ) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . 11
β’ (π β β‘π
β TosetRel ) |
56 | 4 | psrn 18469 |
. . . . . . . . . . . . 13
β’ (π
β PosetRel β π = ran π
) |
57 | 3, 56 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π = ran π
) |
58 | 7, 57 | sseqtrd 3985 |
. . . . . . . . . . 11
β’ (π β π΄ β ran π
) |
59 | 57 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β π = ran π
) |
60 | 59 | rabeqdv 3421 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π
π§ β§ π§π
π¦)} = {π§ β ran π
β£ (π₯π
π§ β§ π§π
π¦)}) |
61 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
62 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π§ β V |
63 | 61, 62 | brcnv 5839 |
. . . . . . . . . . . . . . . 16
β’ (π¦β‘π
π§ β π§π
π¦) |
64 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
65 | 62, 64 | brcnv 5839 |
. . . . . . . . . . . . . . . 16
β’ (π§β‘π
π₯ β π₯π
π§) |
66 | 63, 65 | anbi12ci 629 |
. . . . . . . . . . . . . . 15
β’ ((π¦β‘π
π§ β§ π§β‘π
π₯) β (π₯π
π§ β§ π§π
π¦)) |
67 | 66 | rabbii 3412 |
. . . . . . . . . . . . . 14
β’ {π§ β ran π
β£ (π¦β‘π
π§ β§ π§β‘π
π₯)} = {π§ β ran π
β£ (π₯π
π§ β§ π§π
π¦)} |
68 | 60, 67 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π
π§ β§ π§π
π¦)} = {π§ β ran π
β£ (π¦β‘π
π§ β§ π§β‘π
π₯)}) |
69 | 68, 51 | eqsstrrd 3984 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β ran π
β£ (π¦β‘π
π§ β§ π§β‘π
π₯)} β π΄) |
70 | 69 | ancom2s 649 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΄ β§ π₯ β π΄)) β {π§ β ran π
β£ (π¦β‘π
π§ β§ π§β‘π
π₯)} β π΄) |
71 | 53, 55, 58, 70 | ordtrest2lem 22570 |
. . . . . . . . . 10
β’ (π β βπ£ β ran (π§ β ran π
β¦ {π€ β ran π
β£ Β¬ π€β‘π
π§})(π£ β© π΄) β (ordTopβ(β‘π
β© (π΄ Γ π΄)))) |
72 | | vex 3448 |
. . . . . . . . . . . . . . . . . 18
β’ π€ β V |
73 | 72, 62 | brcnv 5839 |
. . . . . . . . . . . . . . . . 17
β’ (π€β‘π
π§ β π§π
π€) |
74 | 73 | bicomi 223 |
. . . . . . . . . . . . . . . 16
β’ (π§π
π€ β π€β‘π
π§) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π§π
π€ β π€β‘π
π§)) |
76 | 75 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π β (Β¬ π§π
π€ β Β¬ π€β‘π
π§)) |
77 | 57, 76 | rabeqbidv 3423 |
. . . . . . . . . . . . 13
β’ (π β {π€ β π β£ Β¬ π§π
π€} = {π€ β ran π
β£ Β¬ π€β‘π
π§}) |
78 | 57, 77 | mpteq12dv 5197 |
. . . . . . . . . . . 12
β’ (π β (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}) = (π§ β ran π
β¦ {π€ β ran π
β£ Β¬ π€β‘π
π§})) |
79 | 78 | rneqd 5894 |
. . . . . . . . . . 11
β’ (π β ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}) = ran (π§ β ran π
β¦ {π€ β ran π
β£ Β¬ π€β‘π
π§})) |
80 | | psss 18474 |
. . . . . . . . . . . . . . 15
β’ (π
β PosetRel β (π
β© (π΄ Γ π΄)) β PosetRel) |
81 | 3, 80 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π
β© (π΄ Γ π΄)) β PosetRel) |
82 | | ordtcnv 22568 |
. . . . . . . . . . . . . 14
β’ ((π
β© (π΄ Γ π΄)) β PosetRel β
(ordTopββ‘(π
β© (π΄ Γ π΄))) = (ordTopβ(π
β© (π΄ Γ π΄)))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (ordTopββ‘(π
β© (π΄ Γ π΄))) = (ordTopβ(π
β© (π΄ Γ π΄)))) |
84 | | cnvin 6098 |
. . . . . . . . . . . . . . 15
β’ β‘(π
β© (π΄ Γ π΄)) = (β‘π
β© β‘(π΄ Γ π΄)) |
85 | | cnvxp 6110 |
. . . . . . . . . . . . . . . 16
β’ β‘(π΄ Γ π΄) = (π΄ Γ π΄) |
86 | 85 | ineq2i 4170 |
. . . . . . . . . . . . . . 15
β’ (β‘π
β© β‘(π΄ Γ π΄)) = (β‘π
β© (π΄ Γ π΄)) |
87 | 84, 86 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ β‘(π
β© (π΄ Γ π΄)) = (β‘π
β© (π΄ Γ π΄)) |
88 | 87 | fveq2i 6846 |
. . . . . . . . . . . . 13
β’
(ordTopββ‘(π
β© (π΄ Γ π΄))) = (ordTopβ(β‘π
β© (π΄ Γ π΄))) |
89 | 83, 88 | eqtr3di 2788 |
. . . . . . . . . . . 12
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) = (ordTopβ(β‘π
β© (π΄ Γ π΄)))) |
90 | 89 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π β ((π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β (π£ β© π΄) β (ordTopβ(β‘π
β© (π΄ Γ π΄))))) |
91 | 79, 90 | raleqbidv 3318 |
. . . . . . . . . 10
β’ (π β (βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β βπ£ β ran (π§ β ran π
β¦ {π€ β ran π
β£ Β¬ π€β‘π
π§})(π£ β© π΄) β (ordTopβ(β‘π
β© (π΄ Γ π΄))))) |
92 | 71, 91 | mpbird 257 |
. . . . . . . . 9
β’ (π β βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
93 | | ralunb 4152 |
. . . . . . . . 9
β’
(βπ£ β
(ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β (βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§})(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β§ βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))))) |
94 | 52, 92, 93 | sylanbrc 584 |
. . . . . . . 8
β’ (π β βπ£ β (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
95 | | ralunb 4152 |
. . . . . . . 8
β’
(βπ£ β
({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β (βπ£ β {π} (π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β§ βπ£ β (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))))) |
96 | 50, 94, 95 | sylanbrc 584 |
. . . . . . 7
β’ (π β βπ£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
97 | | eqid 2733 |
. . . . . . . 8
β’ (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄)) = (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄)) |
98 | 97 | fmpt 7059 |
. . . . . . 7
β’
(βπ£ β
({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))(π£ β© π΄) β (ordTopβ(π
β© (π΄ Γ π΄))) β (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄)):({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))βΆ(ordTopβ(π
β© (π΄ Γ π΄)))) |
99 | 96, 98 | sylib 217 |
. . . . . 6
β’ (π β (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄)):({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€})))βΆ(ordTopβ(π
β© (π΄ Γ π΄)))) |
100 | 99 | frnd 6677 |
. . . . 5
β’ (π β ran (π£ β ({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) β¦ (π£ β© π΄)) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
101 | 33, 100 | eqsstrd 3983 |
. . . 4
β’ (π β (({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
102 | | tgfiss 22357 |
. . . 4
β’
(((ordTopβ(π
β© (π΄ Γ π΄))) β Top β§ (({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) β (topGenβ(fiβ(({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄))) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
103 | 26, 101, 102 | syl2anc 585 |
. . 3
β’ (π β
(topGenβ(fiβ(({π} βͺ (ran (π§ β π β¦ {π€ β π β£ Β¬ π€π
π§}) βͺ ran (π§ β π β¦ {π€ β π β£ Β¬ π§π
π€}))) βΎt π΄))) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
104 | 22, 103 | eqsstrd 3983 |
. 2
β’ (π β ((ordTopβπ
) βΎt π΄) β (ordTopβ(π
β© (π΄ Γ π΄)))) |
105 | 10, 104 | eqssd 3962 |
1
β’ (π β (ordTopβ(π
β© (π΄ Γ π΄))) = ((ordTopβπ
) βΎt π΄)) |