# Metamath Proof Explorer

## Theorem istopon

Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion istopon ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)↔\left({J}\in \mathrm{Top}\wedge {B}=\bigcup {J}\right)$

### Proof

Step Hyp Ref Expression
1 elfvex ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)\to {B}\in \mathrm{V}$
2 uniexg ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in \mathrm{V}$
3 eleq1 ${⊢}{B}=\bigcup {J}\to \left({B}\in \mathrm{V}↔\bigcup {J}\in \mathrm{V}\right)$
4 2 3 syl5ibrcom ${⊢}{J}\in \mathrm{Top}\to \left({B}=\bigcup {J}\to {B}\in \mathrm{V}\right)$
5 4 imp ${⊢}\left({J}\in \mathrm{Top}\wedge {B}=\bigcup {J}\right)\to {B}\in \mathrm{V}$
6 eqeq1 ${⊢}{b}={B}\to \left({b}=\bigcup {j}↔{B}=\bigcup {j}\right)$
7 6 rabbidv ${⊢}{b}={B}\to \left\{{j}\in \mathrm{Top}|{b}=\bigcup {j}\right\}=\left\{{j}\in \mathrm{Top}|{B}=\bigcup {j}\right\}$
8 df-topon ${⊢}\mathrm{TopOn}=\left({b}\in \mathrm{V}⟼\left\{{j}\in \mathrm{Top}|{b}=\bigcup {j}\right\}\right)$
9 vpwex ${⊢}𝒫{b}\in \mathrm{V}$
10 9 pwex ${⊢}𝒫𝒫{b}\in \mathrm{V}$
11 rabss ${⊢}\left\{{j}\in \mathrm{Top}|{b}=\bigcup {j}\right\}\subseteq 𝒫𝒫{b}↔\forall {j}\in \mathrm{Top}\phantom{\rule{.4em}{0ex}}\left({b}=\bigcup {j}\to {j}\in 𝒫𝒫{b}\right)$
12 pwuni ${⊢}{j}\subseteq 𝒫\bigcup {j}$
13 pweq ${⊢}{b}=\bigcup {j}\to 𝒫{b}=𝒫\bigcup {j}$
14 12 13 sseqtrrid ${⊢}{b}=\bigcup {j}\to {j}\subseteq 𝒫{b}$
15 velpw ${⊢}{j}\in 𝒫𝒫{b}↔{j}\subseteq 𝒫{b}$
16 14 15 sylibr ${⊢}{b}=\bigcup {j}\to {j}\in 𝒫𝒫{b}$
17 16 a1i ${⊢}{j}\in \mathrm{Top}\to \left({b}=\bigcup {j}\to {j}\in 𝒫𝒫{b}\right)$
18 11 17 mprgbir ${⊢}\left\{{j}\in \mathrm{Top}|{b}=\bigcup {j}\right\}\subseteq 𝒫𝒫{b}$
19 10 18 ssexi ${⊢}\left\{{j}\in \mathrm{Top}|{b}=\bigcup {j}\right\}\in \mathrm{V}$
20 7 8 19 fvmpt3i ${⊢}{B}\in \mathrm{V}\to \mathrm{TopOn}\left({B}\right)=\left\{{j}\in \mathrm{Top}|{B}=\bigcup {j}\right\}$
21 20 eleq2d ${⊢}{B}\in \mathrm{V}\to \left({J}\in \mathrm{TopOn}\left({B}\right)↔{J}\in \left\{{j}\in \mathrm{Top}|{B}=\bigcup {j}\right\}\right)$
22 unieq ${⊢}{j}={J}\to \bigcup {j}=\bigcup {J}$
23 22 eqeq2d ${⊢}{j}={J}\to \left({B}=\bigcup {j}↔{B}=\bigcup {J}\right)$
24 23 elrab ${⊢}{J}\in \left\{{j}\in \mathrm{Top}|{B}=\bigcup {j}\right\}↔\left({J}\in \mathrm{Top}\wedge {B}=\bigcup {J}\right)$
25 21 24 syl6bb ${⊢}{B}\in \mathrm{V}\to \left({J}\in \mathrm{TopOn}\left({B}\right)↔\left({J}\in \mathrm{Top}\wedge {B}=\bigcup {J}\right)\right)$
26 1 5 25 pm5.21nii ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)↔\left({J}\in \mathrm{Top}\wedge {B}=\bigcup {J}\right)$