# Metamath Proof Explorer

## Theorem qtoptop2

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion qtoptop2 ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\mathrm{qTop}{F}\in \mathrm{Top}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 1 qtopres ${⊢}{F}\in {V}\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)$
3 2 3ad2ant2 ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)$
4 simp1 ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\in \mathrm{Top}$
5 funres ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}\left({{F}↾}_{\bigcup {J}}\right)$
6 5 3ad2ant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \mathrm{Fun}\left({{F}↾}_{\bigcup {J}}\right)$
7 funforn ${⊢}\mathrm{Fun}\left({{F}↾}_{\bigcup {J}}\right)↔\left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
8 6 7 sylib ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
9 dmres ${⊢}\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)=\bigcup {J}\cap \mathrm{dom}{F}$
10 inss1 ${⊢}\bigcup {J}\cap \mathrm{dom}{F}\subseteq \bigcup {J}$
11 9 10 eqsstri ${⊢}\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}$
12 11 a1i ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}$
13 1 elqtop ${⊢}\left({J}\in \mathrm{Top}\wedge \left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge \mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}\right)\to \left({y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\right)\right)$
14 4 8 12 13 syl3anc ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\right)\right)$
15 14 simprbda ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\to {y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
16 velpw ${⊢}{y}\in 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)↔{y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
17 15 16 sylibr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\to {y}\in 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
18 17 ex ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\to {y}\in 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\right)$
19 18 ssrdv ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\subseteq 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
20 sstr2 ${⊢}{x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\subseteq 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\to {x}\subseteq 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\right)$
21 19 20 syl5com ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to {x}\subseteq 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\right)$
22 sspwuni ${⊢}{x}\subseteq 𝒫\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)↔\bigcup {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
23 21 22 syl6ib ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \bigcup {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\right)$
24 imauni ${⊢}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]=\bigcup _{{y}\in {x}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]$
25 14 simplbda ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
26 25 ralrimiva ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \forall {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
27 ssralv ${⊢}{x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \left(\forall {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\right)$
28 26 27 mpan9 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
29 iunopn ${⊢}\left({J}\in \mathrm{Top}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\right)\to \bigcup _{{y}\in {x}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
30 4 28 29 syl2an2r ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\to \bigcup _{{y}\in {x}}{\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
31 24 30 eqeltrid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]\in {J}$
32 31 ex ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]\in {J}\right)$
33 23 32 jcad ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \left(\bigcup {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]\in {J}\right)\right)$
34 1 elqtop ${⊢}\left({J}\in \mathrm{Top}\wedge \left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge \mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}\right)\to \left(\bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left(\bigcup {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]\in {J}\right)\right)$
35 4 8 12 34 syl3anc ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left(\bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left(\bigcup {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[\bigcup {x}\right]\in {J}\right)\right)$
36 33 35 sylibrd ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)$
37 36 alrimiv ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)$
38 inss1 ${⊢}{x}\cap {y}\subseteq {x}$
39 1 elqtop ${⊢}\left({J}\in \mathrm{Top}\wedge \left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge \mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}\right)\to \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}\right)\right)$
40 4 8 12 39 syl3anc ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}\right)\right)$
41 40 biimpa ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\to \left({x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}\right)$
42 41 adantrr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to \left({x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}\right)$
43 42 simpld ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {x}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
44 38 43 sstrid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {x}\cap {y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)$
45 6 adantr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to \mathrm{Fun}\left({{F}↾}_{\bigcup {J}}\right)$
46 inpreima ${⊢}\mathrm{Fun}\left({{F}↾}_{\bigcup {J}}\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]={\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\cap {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]$
47 45 46 syl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]={\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\cap {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]$
48 4 adantr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {J}\in \mathrm{Top}$
49 42 simprd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}$
50 25 adantrl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
51 inopn ${⊢}\left({J}\in \mathrm{Top}\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\in {J}\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\cap {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
52 48 49 50 51 syl3anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\right]\cap {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{y}\right]\in {J}$
53 47 52 eqeltrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]\in {J}$
54 1 elqtop ${⊢}\left({J}\in \mathrm{Top}\wedge \left({{F}↾}_{\bigcup {J}}\right):\mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\underset{onto}{⟶}\mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge \mathrm{dom}\left({{F}↾}_{\bigcup {J}}\right)\subseteq \bigcup {J}\right)\to \left({x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({x}\cap {y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]\in {J}\right)\right)$
55 4 8 12 54 syl3anc ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \left({x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({x}\cap {y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]\in {J}\right)\right)$
56 55 adantr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to \left({x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)↔\left({x}\cap {y}\subseteq \mathrm{ran}\left({{F}↾}_{\bigcup {J}}\right)\wedge {\left({{F}↾}_{\bigcup {J}}\right)}^{-1}\left[{x}\cap {y}\right]\in {J}\right)\right)$
57 44 53 56 mpbir2and ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\wedge \left({x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\wedge {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)\to {x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)$
58 57 ralrimivva ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to \forall {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)$
59 ovex ${⊢}{J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\in \mathrm{V}$
60 istopg ${⊢}{J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\in \mathrm{V}\to \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\in \mathrm{Top}↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\wedge \forall {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\right)$
61 59 60 ax-mp ${⊢}{J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\in \mathrm{Top}↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\to \bigcup {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)\wedge \forall {x}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \left({J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\right)\right)$
62 37 58 61 sylanbrc ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\mathrm{qTop}\left({{F}↾}_{\bigcup {J}}\right)\in \mathrm{Top}$
63 3 62 eqeltrd ${⊢}\left({J}\in \mathrm{Top}\wedge {F}\in {V}\wedge \mathrm{Fun}{F}\right)\to {J}\mathrm{qTop}{F}\in \mathrm{Top}$