| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ordttopon.3 |
. . . 4
β’ π = dom π
|
| 2 | | eqid 2724 |
. . . 4
β’ ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) |
| 3 | | eqid 2724 |
. . . 4
β’ ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}) = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}) |
| 4 | 1, 2, 3 | ordtval 23014 |
. . 3
β’ (π
β π β (ordTopβπ
) = (topGenβ(fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))))) |
| 5 | | fibas 22801 |
. . . 4
β’
(fiβ({π} βͺ
(ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))) β TopBases |
| 6 | | tgtopon 22795 |
. . . 4
β’
((fiβ({π}
βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))) β TopBases β
(topGenβ(fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) β (TopOnββͺ (fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))))) |
| 7 | 5, 6 | ax-mp 5 |
. . 3
β’
(topGenβ(fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) β (TopOnββͺ (fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) |
| 8 | 4, 7 | eqeltrdi 2833 |
. 2
β’ (π
β π β (ordTopβπ
) β (TopOnββͺ (fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))))) |
| 9 | 1, 2, 3 | ordtuni 23015 |
. . . 4
β’ (π
β π β π = βͺ ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))) |
| 10 | | dmexg 7887 |
. . . . . . . 8
β’ (π
β π β dom π
β V) |
| 11 | 1, 10 | eqeltrid 2829 |
. . . . . . 7
β’ (π
β π β π β V) |
| 12 | 9, 11 | eqeltrrd 2826 |
. . . . . 6
β’ (π
β π β βͺ ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) β V) |
| 13 | | uniexb 7744 |
. . . . . 6
β’ (({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) β V β βͺ ({π}
βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) β V) |
| 14 | 12, 13 | sylibr 233 |
. . . . 5
β’ (π
β π β ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) β V) |
| 15 | | fiuni 9418 |
. . . . 5
β’ (({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) β V β βͺ ({π}
βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) = βͺ
(fiβ({π} βͺ (ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) |
| 16 | 14, 15 | syl 17 |
. . . 4
β’ (π
β π β βͺ ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))) = βͺ
(fiβ({π} βͺ (ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) |
| 17 | 9, 16 | eqtrd 2764 |
. . 3
β’ (π
β π β π = βͺ
(fiβ({π} βͺ (ran
(π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦}))))) |
| 18 | 17 | fveq2d 6885 |
. 2
β’ (π
β π β (TopOnβπ) = (TopOnββͺ (fiβ({π} βͺ (ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π
π¦})))))) |
| 19 | 8, 18 | eleqtrrd 2828 |
1
β’ (π
β π β (ordTopβπ
) β (TopOnβπ)) |
