Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ⊆
wss 3949 ∪ cuni 4909 Topctop 22395 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 ax-sep 5300 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-in 3956 df-ss 3966 df-pw 4605 df-uni 4910 df-top 22396 |
This theorem is referenced by: riinopn
22410 toponmax
22428 cldval
22527 ntrfval
22528 clsfval
22529 iscld
22531 ntrval
22540 clsval
22541 0cld
22542 clsval2
22554 ntrtop
22574 toponmre
22597 neifval
22603 neif
22604 neival
22606 isnei
22607 tpnei
22625 lpfval
22642 lpval
22643 restcld
22676 restcls
22685 restntr
22686 cnrest
22789 cmpsub
22904 hauscmplem
22910 cmpfi
22912 isconn2
22918 connsubclo
22928 1stcfb
22949 1stcelcls
22965 islly2
22988 lly1stc
23000 islocfin
23021 finlocfin
23024 cmpkgen
23055 llycmpkgen
23056 ptbasid
23079 ptpjpre2
23084 ptopn2
23088 xkoopn
23093 xkouni
23103 txcld
23107 txcn
23130 ptrescn
23143 txtube
23144 txhaus
23151 xkoptsub
23158 xkopt
23159 xkopjcn
23160 qtoptop
23204 qtopuni
23206 opnfbas
23346 flimval
23467 flimfil
23473 hausflim
23485 hauspwpwf1
23491 hauspwpwdom
23492 flimfnfcls
23532 cnpfcfi
23544 bcthlem5
24845 dvply1
25797 cldssbrsiga
33185 dya2iocucvr
33283 kur14lem7
34203 kur14lem9
34205 connpconn
34226 cvmliftmolem1
34272 ordtop
35321 pibt2
36298 ntrelmap
42876 clselmap
42878 dssmapntrcls
42879 dssmapclsntr
42880 toprestsubel
43848 reopn
43999 toplatglb0
47624 |