| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ordttopon.3 |
. . . . . . . . 9
β’ π = dom π
|
| 2 | | eqid 2726 |
. . . . . . . . 9
β’ ran
(π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) = ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) |
| 3 | | eqid 2726 |
. . . . . . . . 9
β’ ran
(π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) = ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) |
| 4 | 1, 2, 3 | ordtuni 23049 |
. . . . . . . 8
β’ (π
β π β π = βͺ ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) |
| 5 | 4 | adantr 480 |
. . . . . . 7
β’ ((π
β π β§ π β π) β π = βͺ ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) |
| 6 | | dmexg 7891 |
. . . . . . . . 9
β’ (π
β π β dom π
β V) |
| 7 | 1, 6 | eqeltrid 2831 |
. . . . . . . 8
β’ (π
β π β π β V) |
| 8 | 7 | adantr 480 |
. . . . . . 7
β’ ((π
β π β§ π β π) β π β V) |
| 9 | 5, 8 | eqeltrrd 2828 |
. . . . . 6
β’ ((π
β π β§ π β π) β βͺ
({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β V) |
| 10 | | uniexb 7748 |
. . . . . 6
β’ (({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β V β βͺ ({π}
βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β V) |
| 11 | 9, 10 | sylibr 233 |
. . . . 5
β’ ((π
β π β§ π β π) β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β V) |
| 12 | | ssfii 9416 |
. . . . 5
β’ (({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β V β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β (fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))))) |
| 13 | 11, 12 | syl 17 |
. . . 4
β’ ((π
β π β§ π β π) β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β (fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))))) |
| 14 | | fibas 22835 |
. . . . 5
β’
(fiβ({π} βͺ
(ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) β TopBases |
| 15 | | bastg 22824 |
. . . . 5
β’
((fiβ({π}
βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) β TopBases β
(fiβ({π} βͺ (ran
(π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) β (topGenβ(fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))))) |
| 16 | 14, 15 | ax-mp 5 |
. . . 4
β’
(fiβ({π} βͺ
(ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) β (topGenβ(fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))))) |
| 17 | 13, 16 | sstrdi 3989 |
. . 3
β’ ((π
β π β§ π β π) β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β (topGenβ(fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))))) |
| 18 | 1, 2, 3 | ordtval 23048 |
. . . 4
β’ (π
β π β (ordTopβπ
) = (topGenβ(fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))))) |
| 19 | 18 | adantr 480 |
. . 3
β’ ((π
β π β§ π β π) β (ordTopβπ
) = (topGenβ(fiβ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))))) |
| 20 | 17, 19 | sseqtrrd 4018 |
. 2
β’ ((π
β π β§ π β π) β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) β (ordTopβπ
)) |
| 21 | | ssun2 4168 |
. . 3
β’ (ran
(π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})) β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) |
| 22 | | ssun2 4168 |
. . . 4
β’ ran
(π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) β (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})) |
| 23 | | simpr 484 |
. . . . . 6
β’ ((π
β π β§ π β π) β π β π) |
| 24 | | eqidd 2727 |
. . . . . 6
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ ππ
π₯}) |
| 25 | | breq1 5144 |
. . . . . . . . 9
β’ (π¦ = π β (π¦π
π₯ β ππ
π₯)) |
| 26 | 25 | notbid 318 |
. . . . . . . 8
β’ (π¦ = π β (Β¬ π¦π
π₯ β Β¬ ππ
π₯)) |
| 27 | 26 | rabbidv 3434 |
. . . . . . 7
β’ (π¦ = π β {π₯ β π β£ Β¬ π¦π
π₯} = {π₯ β π β£ Β¬ ππ
π₯}) |
| 28 | 27 | rspceeqv 3628 |
. . . . . 6
β’ ((π β π β§ {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ ππ
π₯}) β βπ¦ β π {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ π¦π
π₯}) |
| 29 | 23, 24, 28 | syl2anc 583 |
. . . . 5
β’ ((π
β π β§ π β π) β βπ¦ β π {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ π¦π
π₯}) |
| 30 | | rabexg 5324 |
. . . . . 6
β’ (π β V β {π₯ β π β£ Β¬ ππ
π₯} β V) |
| 31 | | eqid 2726 |
. . . . . . 7
β’ (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) = (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) |
| 32 | 31 | elrnmpt 5949 |
. . . . . 6
β’ ({π₯ β π β£ Β¬ ππ
π₯} β V β ({π₯ β π β£ Β¬ ππ
π₯} β ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) β βπ¦ β π {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ π¦π
π₯})) |
| 33 | 8, 30, 32 | 3syl 18 |
. . . . 5
β’ ((π
β π β§ π β π) β ({π₯ β π β£ Β¬ ππ
π₯} β ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}) β βπ¦ β π {π₯ β π β£ Β¬ ππ
π₯} = {π₯ β π β£ Β¬ π¦π
π₯})) |
| 34 | 29, 33 | mpbird 257 |
. . . 4
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} β ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})) |
| 35 | 22, 34 | sselid 3975 |
. . 3
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} β (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯}))) |
| 36 | 21, 35 | sselid 3975 |
. 2
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} β ({π} βͺ (ran (π¦ β π β¦ {π₯ β π β£ Β¬ π₯π
π¦}) βͺ ran (π¦ β π β¦ {π₯ β π β£ Β¬ π¦π
π₯})))) |
| 37 | 20, 36 | sseldd 3978 |
1
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} β (ordTopβπ
)) |
