Step | Hyp | Ref
| Expression |
1 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π¦ β V |
2 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π₯ β V |
3 | 1, 2 | brcnv 5843 |
. . . . . . . . . . . 12
β’ (π¦β‘ β€ π₯ β π₯ β€ π¦) |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (πΎ β Proset β (π¦β‘ β€ π₯ β π₯ β€ π¦)) |
5 | 4 | notbid 318 |
. . . . . . . . . 10
β’ (πΎ β Proset β (Β¬
π¦β‘ β€ π₯ β Β¬ π₯ β€ π¦)) |
6 | 5 | rabbidv 3418 |
. . . . . . . . 9
β’ (πΎ β Proset β {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯} = {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) |
7 | 6 | mpteq2dv 5212 |
. . . . . . . 8
β’ (πΎ β Proset β (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) = (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})) |
8 | 7 | rneqd 5898 |
. . . . . . 7
β’ (πΎ β Proset β ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})) |
9 | 2, 1 | brcnv 5843 |
. . . . . . . . . . . 12
β’ (π₯β‘ β€ π¦ β π¦ β€ π₯) |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
β’ (πΎ β Proset β (π₯β‘ β€ π¦ β π¦ β€ π₯)) |
11 | 10 | notbid 318 |
. . . . . . . . . 10
β’ (πΎ β Proset β (Β¬
π₯β‘ β€ π¦ β Β¬ π¦ β€ π₯)) |
12 | 11 | rabbidv 3418 |
. . . . . . . . 9
β’ (πΎ β Proset β {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦} = {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) |
13 | 12 | mpteq2dv 5212 |
. . . . . . . 8
β’ (πΎ β Proset β (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}) = (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯})) |
14 | 13 | rneqd 5898 |
. . . . . . 7
β’ (πΎ β Proset β ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯})) |
15 | 8, 14 | uneq12d 4129 |
. . . . . 6
β’ (πΎ β Proset β (ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦})) = (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}))) |
16 | | uncom 4118 |
. . . . . 6
β’ (ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯})) = (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})) |
17 | 15, 16 | eqtrdi 2793 |
. . . . 5
β’ (πΎ β Proset β (ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦})) = (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}))) |
18 | 17 | uneq2d 4128 |
. . . 4
β’ (πΎ β Proset β ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}))) = ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})))) |
19 | 18 | fveq2d 6851 |
. . 3
β’ (πΎ β Proset β
(fiβ({π΅} βͺ (ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦})))) = (fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}))))) |
20 | 19 | fveq2d 6851 |
. 2
β’ (πΎ β Proset β
(topGenβ(fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}))))) =
(topGenβ(fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})))))) |
21 | | eqid 2737 |
. . . 4
β’
(ODualβπΎ) =
(ODualβπΎ) |
22 | 21 | oduprs 31866 |
. . 3
β’ (πΎ β Proset β
(ODualβπΎ) β
Proset ) |
23 | | ordtNEW.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
24 | 21, 23 | odubas 18187 |
. . . 4
β’ π΅ =
(Baseβ(ODualβπΎ)) |
25 | | ordtNEW.l |
. . . . . 6
β’ β€ =
((leβπΎ) β© (π΅ Γ π΅)) |
26 | 25 | cnveqi 5835 |
. . . . 5
β’ β‘ β€ = β‘((leβπΎ) β© (π΅ Γ π΅)) |
27 | | cnvin 6102 |
. . . . 5
β’ β‘((leβπΎ) β© (π΅ Γ π΅)) = (β‘(leβπΎ) β© β‘(π΅ Γ π΅)) |
28 | | eqid 2737 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
29 | 21, 28 | oduleval 18185 |
. . . . . 6
β’ β‘(leβπΎ) = (leβ(ODualβπΎ)) |
30 | | cnvxp 6114 |
. . . . . 6
β’ β‘(π΅ Γ π΅) = (π΅ Γ π΅) |
31 | 29, 30 | ineq12i 4175 |
. . . . 5
β’ (β‘(leβπΎ) β© β‘(π΅ Γ π΅)) = ((leβ(ODualβπΎ)) β© (π΅ Γ π΅)) |
32 | 26, 27, 31 | 3eqtri 2769 |
. . . 4
β’ β‘ β€ =
((leβ(ODualβπΎ))
β© (π΅ Γ π΅)) |
33 | | eqid 2737 |
. . . 4
β’ ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) |
34 | | eqid 2737 |
. . . 4
β’ ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦}) |
35 | 24, 32, 33, 34 | ordtprsval 32539 |
. . 3
β’
((ODualβπΎ)
β Proset β (ordTopββ‘
β€ ) =
(topGenβ(fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦})))))) |
36 | 22, 35 | syl 17 |
. 2
β’ (πΎ β Proset β
(ordTopββ‘ β€ ) =
(topGenβ(fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦β‘
β€
π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯β‘
β€
π¦})))))) |
37 | | eqid 2737 |
. . 3
β’ ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) |
38 | | eqid 2737 |
. . 3
β’ ran
(π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) |
39 | 23, 25, 37, 38 | ordtprsval 32539 |
. 2
β’ (πΎ β Proset β
(ordTopβ β€ ) =
(topGenβ(fiβ({π΅} βͺ (ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) βͺ ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦})))))) |
40 | 20, 36, 39 | 3eqtr4d 2787 |
1
β’ (πΎ β Proset β
(ordTopββ‘ β€ ) = (ordTopβ
β€
)) |