Step | Hyp | Ref
| Expression |
1 | | ordtrest2NEW.2 |
. . . 4
β’ (π β πΎ β Toset) |
2 | | tospos 18316 |
. . . 4
β’ (πΎ β Toset β πΎ β Poset) |
3 | | posprs 18212 |
. . . 4
β’ (πΎ β Poset β πΎ β Proset
) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
β’ (π β πΎ β Proset ) |
5 | | ordtrest2NEW.3 |
. . 3
β’ (π β π΄ β π΅) |
6 | | ordtNEW.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
7 | | ordtNEW.l |
. . . 4
β’ β€ =
((leβπΎ) β© (π΅ Γ π΅)) |
8 | 6, 7 | ordtrestNEW 32542 |
. . 3
β’ ((πΎ β Proset β§ π΄ β π΅) β (ordTopβ( β€ β© (π΄ Γ π΄))) β ((ordTopβ β€ )
βΎt π΄)) |
9 | 4, 5, 8 | syl2anc 585 |
. 2
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) β ((ordTopβ
β€ )
βΎt π΄)) |
10 | | eqid 2737 |
. . . . . . . 8
β’ ran
(π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) = ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) |
11 | | eqid 2737 |
. . . . . . . 8
β’ ran
(π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}) = ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}) |
12 | 6, 7, 10, 11 | ordtprsval 32539 |
. . . . . . 7
β’ (πΎ β Proset β
(ordTopβ β€ ) =
(topGenβ(fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))))) |
13 | 4, 12 | syl 17 |
. . . . . 6
β’ (π β (ordTopβ β€ ) =
(topGenβ(fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))))) |
14 | 13 | oveq1d 7377 |
. . . . 5
β’ (π β ((ordTopβ β€ )
βΎt π΄) =
((topGenβ(fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))))) βΎt π΄)) |
15 | | fibas 22343 |
. . . . . 6
β’
(fiβ({π΅} βͺ
(ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) β TopBases |
16 | 6 | fvexi 6861 |
. . . . . . . 8
β’ π΅ β V |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (π β π΅ β V) |
18 | 17, 5 | ssexd 5286 |
. . . . . 6
β’ (π β π΄ β V) |
19 | | tgrest 22526 |
. . . . . 6
β’
(((fiβ({π΅}
βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) β TopBases β§ π΄ β V) β
(topGenβ((fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) βΎt π΄)) = ((topGenβ(fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))))) βΎt π΄)) |
20 | 15, 18, 19 | sylancr 588 |
. . . . 5
β’ (π β
(topGenβ((fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) βΎt π΄)) = ((topGenβ(fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))))) βΎt π΄)) |
21 | 14, 20 | eqtr4d 2780 |
. . . 4
β’ (π β ((ordTopβ β€ )
βΎt π΄) =
(topGenβ((fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) βΎt π΄))) |
22 | | firest 17321 |
. . . . 5
β’
(fiβ(({π΅}
βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄)) = ((fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) βΎt π΄) |
23 | 22 | fveq2i 6850 |
. . . 4
β’
(topGenβ(fiβ(({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄))) = (topGenβ((fiβ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) βΎt π΄)) |
24 | 21, 23 | eqtr4di 2795 |
. . 3
β’ (π β ((ordTopβ β€ )
βΎt π΄) =
(topGenβ(fiβ(({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄)))) |
25 | | fvex 6860 |
. . . . . . . 8
β’
(leβπΎ) β
V |
26 | 25 | inex1 5279 |
. . . . . . 7
β’
((leβπΎ) β©
(π΅ Γ π΅)) β V |
27 | 7, 26 | eqeltri 2834 |
. . . . . 6
β’ β€ β
V |
28 | 27 | inex1 5279 |
. . . . 5
β’ ( β€ β©
(π΄ Γ π΄)) β V |
29 | | ordttop 22567 |
. . . . 5
β’ (( β€ β©
(π΄ Γ π΄)) β V β
(ordTopβ( β€ β© (π΄ Γ π΄))) β Top) |
30 | 28, 29 | mp1i 13 |
. . . 4
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) β Top) |
31 | 6, 7, 10, 11 | ordtprsuni 32540 |
. . . . . . . . 9
β’ (πΎ β Proset β π΅ = βͺ
({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) |
32 | 4, 31 | syl 17 |
. . . . . . . 8
β’ (π β π΅ = βͺ ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))) |
33 | 32, 17 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β βͺ ({π΅}
βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β V) |
34 | | uniexb 7703 |
. . . . . . 7
β’ (({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β V β βͺ ({π΅}
βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β V) |
35 | 33, 34 | sylibr 233 |
. . . . . 6
β’ (π β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β V) |
36 | | restval 17315 |
. . . . . 6
β’ ((({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β V β§ π΄ β V) β (({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄) = ran (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄))) |
37 | 35, 18, 36 | syl2anc 585 |
. . . . 5
β’ (π β (({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄) = ran (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄))) |
38 | | sseqin2 4180 |
. . . . . . . . . . . 12
β’ (π΄ β π΅ β (π΅ β© π΄) = π΄) |
39 | 5, 38 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π΅ β© π΄) = π΄) |
40 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ dom (
β€
β© (π΄ Γ π΄)) = dom ( β€ β© (π΄ Γ π΄)) |
41 | 40 | ordttopon 22560 |
. . . . . . . . . . . . . 14
β’ (( β€ β©
(π΄ Γ π΄)) β V β
(ordTopβ( β€ β© (π΄ Γ π΄))) β (TopOnβdom ( β€ β©
(π΄ Γ π΄)))) |
42 | 28, 41 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) β (TopOnβdom (
β€
β© (π΄ Γ π΄)))) |
43 | 6, 7 | prsssdm 32538 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Proset β§ π΄ β π΅) β dom ( β€ β© (π΄ Γ π΄)) = π΄) |
44 | 4, 5, 43 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β dom ( β€ β© (π΄ Γ π΄)) = π΄) |
45 | 44 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (TopOnβdom ( β€ β©
(π΄ Γ π΄))) = (TopOnβπ΄)) |
46 | 42, 45 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) β (TopOnβπ΄)) |
47 | | toponmax 22291 |
. . . . . . . . . . . 12
β’
((ordTopβ( β€ β© (π΄ Γ π΄))) β (TopOnβπ΄) β π΄ β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . 11
β’ (π β π΄ β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
49 | 39, 48 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (π β (π΅ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
50 | | elsni 4608 |
. . . . . . . . . . . 12
β’ (π£ β {π΅} β π£ = π΅) |
51 | 50 | ineq1d 4176 |
. . . . . . . . . . 11
β’ (π£ β {π΅} β (π£ β© π΄) = (π΅ β© π΄)) |
52 | 51 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π£ β {π΅} β ((π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β (π΅ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))))) |
53 | 49, 52 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (π β (π£ β {π΅} β (π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))))) |
54 | 53 | ralrimiv 3143 |
. . . . . . . 8
β’ (π β βπ£ β {π΅} (π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
55 | | ordtrest2NEW.4 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π΅ β£ (π₯ β€ π§ β§ π§ β€ π¦)} β π΄) |
56 | 6, 7, 1, 5, 55 | ordtrest2NEWlem 32543 |
. . . . . . . . 9
β’ (π β βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§})(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
57 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(ODualβπΎ) =
(ODualβπΎ) |
58 | 57, 6 | odubas 18187 |
. . . . . . . . . . 11
β’ π΅ =
(Baseβ(ODualβπΎ)) |
59 | 7 | cnveqi 5835 |
. . . . . . . . . . . 12
β’ β‘ β€ = β‘((leβπΎ) β© (π΅ Γ π΅)) |
60 | | cnvin 6102 |
. . . . . . . . . . . . 13
β’ β‘((leβπΎ) β© (π΅ Γ π΅)) = (β‘(leβπΎ) β© β‘(π΅ Γ π΅)) |
61 | | cnvxp 6114 |
. . . . . . . . . . . . . 14
β’ β‘(π΅ Γ π΅) = (π΅ Γ π΅) |
62 | 61 | ineq2i 4174 |
. . . . . . . . . . . . 13
β’ (β‘(leβπΎ) β© β‘(π΅ Γ π΅)) = (β‘(leβπΎ) β© (π΅ Γ π΅)) |
63 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(leβπΎ) =
(leβπΎ) |
64 | 57, 63 | oduleval 18185 |
. . . . . . . . . . . . . 14
β’ β‘(leβπΎ) = (leβ(ODualβπΎ)) |
65 | 64 | ineq1i 4173 |
. . . . . . . . . . . . 13
β’ (β‘(leβπΎ) β© (π΅ Γ π΅)) = ((leβ(ODualβπΎ)) β© (π΅ Γ π΅)) |
66 | 60, 62, 65 | 3eqtri 2769 |
. . . . . . . . . . . 12
β’ β‘((leβπΎ) β© (π΅ Γ π΅)) = ((leβ(ODualβπΎ)) β© (π΅ Γ π΅)) |
67 | 59, 66 | eqtri 2765 |
. . . . . . . . . . 11
β’ β‘ β€ =
((leβ(ODualβπΎ))
β© (π΅ Γ π΅)) |
68 | 57 | odutos 31870 |
. . . . . . . . . . . 12
β’ (πΎ β Toset β
(ODualβπΎ) β
Toset) |
69 | 1, 68 | syl 17 |
. . . . . . . . . . 11
β’ (π β (ODualβπΎ) β Toset) |
70 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π¦ β V |
71 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π§ β V |
72 | 70, 71 | brcnv 5843 |
. . . . . . . . . . . . . . 15
β’ (π¦β‘ β€ π§ β π§ β€ π¦) |
73 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π₯ β V |
74 | 71, 73 | brcnv 5843 |
. . . . . . . . . . . . . . 15
β’ (π§β‘ β€ π₯ β π₯ β€ π§) |
75 | 72, 74 | anbi12ci 629 |
. . . . . . . . . . . . . 14
β’ ((π¦β‘ β€ π§ β§ π§β‘
β€
π₯) β (π₯ β€ π§ β§ π§ β€ π¦)) |
76 | 75 | rabbii 3416 |
. . . . . . . . . . . . 13
β’ {π§ β π΅ β£ (π¦β‘
β€
π§ β§ π§β‘
β€
π₯)} = {π§ β π΅ β£ (π₯ β€ π§ β§ π§ β€ π¦)} |
77 | 76, 55 | eqsstrid 3997 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π΅ β£ (π¦β‘
β€
π§ β§ π§β‘
β€
π₯)} β π΄) |
78 | 77 | ancom2s 649 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΄ β§ π₯ β π΄)) β {π§ β π΅ β£ (π¦β‘
β€
π§ β§ π§β‘
β€
π₯)} β π΄) |
79 | 58, 67, 69, 5, 78 | ordtrest2NEWlem 32543 |
. . . . . . . . . 10
β’ (π β βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€β‘
β€
π§})(π£ β© π΄) β (ordTopβ(β‘ β€ β© (π΄ Γ π΄)))) |
80 | | vex 3452 |
. . . . . . . . . . . . . . . . . 18
β’ π€ β V |
81 | 80, 71 | brcnv 5843 |
. . . . . . . . . . . . . . . . 17
β’ (π€β‘ β€ π§ β π§ β€ π€) |
82 | 81 | bicomi 223 |
. . . . . . . . . . . . . . . 16
β’ (π§ β€ π€ β π€β‘
β€
π§) |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π§ β€ π€ β π€β‘
β€
π§)) |
84 | 83 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π β (Β¬ π§ β€ π€ β Β¬ π€β‘
β€
π§)) |
85 | 84 | rabbidv 3418 |
. . . . . . . . . . . . 13
β’ (π β {π€ β π΅ β£ Β¬ π§ β€ π€} = {π€ β π΅ β£ Β¬ π€β‘
β€
π§}) |
86 | 85 | mpteq2dv 5212 |
. . . . . . . . . . . 12
β’ (π β (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}) = (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€β‘
β€
π§})) |
87 | 86 | rneqd 5898 |
. . . . . . . . . . 11
β’ (π β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}) = ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€β‘
β€
π§})) |
88 | 6 | ressprs 31865 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Proset β§ π΄ β π΅) β (πΎ βΎs π΄) β Proset ) |
89 | 4, 5, 88 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πΎ βΎs π΄) β Proset ) |
90 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(Baseβ(πΎ
βΎs π΄)) =
(Baseβ(πΎ
βΎs π΄)) |
91 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
((leβ(πΎ
βΎs π΄))
β© ((Baseβ(πΎ
βΎs π΄))
Γ (Baseβ(πΎ
βΎs π΄)))) =
((leβ(πΎ
βΎs π΄))
β© ((Baseβ(πΎ
βΎs π΄))
Γ (Baseβ(πΎ
βΎs π΄)))) |
92 | 90, 91 | ordtcnvNEW 32541 |
. . . . . . . . . . . . . . 15
β’ ((πΎ βΎs π΄) β Proset β
(ordTopββ‘((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄))))) =
(ordTopβ((leβ(πΎ
βΎs π΄))
β© ((Baseβ(πΎ
βΎs π΄))
Γ (Baseβ(πΎ
βΎs π΄)))))) |
93 | 89, 92 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (ordTopββ‘((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄))))) = (ordTopβ((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄)))))) |
94 | 6, 7 | prsss 32537 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Proset β§ π΄ β π΅) β ( β€ β© (π΄ Γ π΄)) = ((leβπΎ) β© (π΄ Γ π΄))) |
95 | 4, 5, 94 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β ( β€ β© (π΄ Γ π΄)) = ((leβπΎ) β© (π΄ Γ π΄))) |
96 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΎ βΎs π΄) = (πΎ βΎs π΄) |
97 | 96, 63 | ressle 17268 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β V β (leβπΎ) = (leβ(πΎ βΎs π΄))) |
98 | 18, 97 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (leβπΎ) = (leβ(πΎ βΎs π΄))) |
99 | 96, 6 | ressbas2 17127 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β π΅ β π΄ = (Baseβ(πΎ βΎs π΄))) |
100 | 5, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ = (Baseβ(πΎ βΎs π΄))) |
101 | 100 | sqxpeqd 5670 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ Γ π΄) = ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄)))) |
102 | 98, 101 | ineq12d 4178 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((leβπΎ) β© (π΄ Γ π΄)) = ((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄))))) |
103 | 95, 102 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β ( β€ β© (π΄ Γ π΄)) = ((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄))))) |
104 | 103 | cnveqd 5836 |
. . . . . . . . . . . . . . 15
β’ (π β β‘( β€ β© (π΄ Γ π΄)) = β‘((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄))))) |
105 | 104 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β (ordTopββ‘( β€ β© (π΄ Γ π΄))) = (ordTopββ‘((leβ(πΎ βΎs π΄)) β© ((Baseβ(πΎ βΎs π΄)) Γ (Baseβ(πΎ βΎs π΄)))))) |
106 | 103 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) =
(ordTopβ((leβ(πΎ
βΎs π΄))
β© ((Baseβ(πΎ
βΎs π΄))
Γ (Baseβ(πΎ
βΎs π΄)))))) |
107 | 93, 105, 106 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
β’ (π β (ordTopββ‘( β€ β© (π΄ Γ π΄))) = (ordTopβ( β€ β© (π΄ Γ π΄)))) |
108 | | cnvin 6102 |
. . . . . . . . . . . . . . 15
β’ β‘( β€ β© (π΄ Γ π΄)) = (β‘ β€ β© β‘(π΄ Γ π΄)) |
109 | | cnvxp 6114 |
. . . . . . . . . . . . . . . 16
β’ β‘(π΄ Γ π΄) = (π΄ Γ π΄) |
110 | 109 | ineq2i 4174 |
. . . . . . . . . . . . . . 15
β’ (β‘ β€ β© β‘(π΄ Γ π΄)) = (β‘ β€ β© (π΄ Γ π΄)) |
111 | 108, 110 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ β‘( β€ β© (π΄ Γ π΄)) = (β‘ β€ β© (π΄ Γ π΄)) |
112 | 111 | fveq2i 6850 |
. . . . . . . . . . . . 13
β’
(ordTopββ‘( β€ β©
(π΄ Γ π΄))) = (ordTopβ(β‘ β€ β© (π΄ Γ π΄))) |
113 | 107, 112 | eqtr3di 2792 |
. . . . . . . . . . . 12
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) = (ordTopβ(β‘ β€ β© (π΄ Γ π΄)))) |
114 | 113 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π β ((π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β (π£ β© π΄) β (ordTopβ(β‘ β€ β© (π΄ Γ π΄))))) |
115 | 87, 114 | raleqbidv 3322 |
. . . . . . . . . 10
β’ (π β (βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€β‘
β€
π§})(π£ β© π΄) β (ordTopβ(β‘ β€ β© (π΄ Γ π΄))))) |
116 | 79, 115 | mpbird 257 |
. . . . . . . . 9
β’ (π β βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
117 | | ralunb 4156 |
. . . . . . . . 9
β’
(βπ£ β
(ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β (βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§})(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β§ βπ£ β ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))))) |
118 | 56, 116, 117 | sylanbrc 584 |
. . . . . . . 8
β’ (π β βπ£ β (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
119 | | ralunb 4156 |
. . . . . . . 8
β’
(βπ£ β
({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β (βπ£ β {π΅} (π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β§ βπ£ β (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))))) |
120 | 54, 118, 119 | sylanbrc 584 |
. . . . . . 7
β’ (π β βπ£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
121 | | eqid 2737 |
. . . . . . . 8
β’ (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄)) = (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄)) |
122 | 121 | fmpt 7063 |
. . . . . . 7
β’
(βπ£ β
({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))(π£ β© π΄) β (ordTopβ( β€ β© (π΄ Γ π΄))) β (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄)):({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))βΆ(ordTopβ( β€ β©
(π΄ Γ π΄)))) |
123 | 120, 122 | sylib 217 |
. . . . . 6
β’ (π β (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄)):({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€})))βΆ(ordTopβ( β€ β©
(π΄ Γ π΄)))) |
124 | 123 | frnd 6681 |
. . . . 5
β’ (π β ran (π£ β ({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) β¦ (π£ β© π΄)) β (ordTopβ( β€ β©
(π΄ Γ π΄)))) |
125 | 37, 124 | eqsstrd 3987 |
. . . 4
β’ (π β (({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
126 | | tgfiss 22357 |
. . . 4
β’
(((ordTopβ( β€ β© (π΄ Γ π΄))) β Top β§ (({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄) β (ordTopβ( β€ β© (π΄ Γ π΄)))) β (topGenβ(fiβ(({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄))) β (ordTopβ( β€ β©
(π΄ Γ π΄)))) |
127 | 30, 125, 126 | syl2anc 585 |
. . 3
β’ (π β
(topGenβ(fiβ(({π΅} βͺ (ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π€ β€ π§}) βͺ ran (π§ β π΅ β¦ {π€ β π΅ β£ Β¬ π§ β€ π€}))) βΎt π΄))) β (ordTopβ( β€ β©
(π΄ Γ π΄)))) |
128 | 24, 127 | eqsstrd 3987 |
. 2
β’ (π β ((ordTopβ β€ )
βΎt π΄)
β (ordTopβ( β€ β© (π΄ Γ π΄)))) |
129 | 9, 128 | eqssd 3966 |
1
β’ (π β (ordTopβ( β€ β©
(π΄ Γ π΄))) = ((ordTopβ β€ )
βΎt π΄)) |