Metamath Proof Explorer

Theorem qtopval

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 ${⊢}{X}=\bigcup {J}$
Assertion qtopval ${⊢}\left({J}\in {V}\wedge {F}\in {W}\right)\to {J}\mathrm{qTop}{F}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$

Proof

Step Hyp Ref Expression
1 qtopval.1 ${⊢}{X}=\bigcup {J}$
2 elex ${⊢}{J}\in {V}\to {J}\in \mathrm{V}$
3 elex ${⊢}{F}\in {W}\to {F}\in \mathrm{V}$
4 imaexg ${⊢}{F}\in \mathrm{V}\to {F}\left[{X}\right]\in \mathrm{V}$
5 pwexg ${⊢}{F}\left[{X}\right]\in \mathrm{V}\to 𝒫{F}\left[{X}\right]\in \mathrm{V}$
6 rabexg ${⊢}𝒫{F}\left[{X}\right]\in \mathrm{V}\to \left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}\in \mathrm{V}$
7 4 5 6 3syl ${⊢}{F}\in \mathrm{V}\to \left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}\in \mathrm{V}$
8 7 adantl ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in \mathrm{V}\right)\to \left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}\in \mathrm{V}$
9 simpr ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {f}={F}$
10 simpl ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {j}={J}$
11 10 unieqd ${⊢}\left({j}={J}\wedge {f}={F}\right)\to \bigcup {j}=\bigcup {J}$
12 11 1 syl6eqr ${⊢}\left({j}={J}\wedge {f}={F}\right)\to \bigcup {j}={X}$
13 9 12 imaeq12d ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {f}\left[\bigcup {j}\right]={F}\left[{X}\right]$
14 13 pweqd ${⊢}\left({j}={J}\wedge {f}={F}\right)\to 𝒫{f}\left[\bigcup {j}\right]=𝒫{F}\left[{X}\right]$
15 9 cnveqd ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {{f}}^{-1}={{F}}^{-1}$
16 15 imaeq1d ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {{f}}^{-1}\left[{s}\right]={{F}}^{-1}\left[{s}\right]$
17 16 12 ineq12d ${⊢}\left({j}={J}\wedge {f}={F}\right)\to {{f}}^{-1}\left[{s}\right]\cap \bigcup {j}={{F}}^{-1}\left[{s}\right]\cap {X}$
18 17 10 eleq12d ${⊢}\left({j}={J}\wedge {f}={F}\right)\to \left({{f}}^{-1}\left[{s}\right]\cap \bigcup {j}\in {j}↔{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right)$
19 14 18 rabeqbidv ${⊢}\left({j}={J}\wedge {f}={F}\right)\to \left\{{s}\in 𝒫{f}\left[\bigcup {j}\right]|{{f}}^{-1}\left[{s}\right]\cap \bigcup {j}\in {j}\right\}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
20 df-qtop ${⊢}\mathrm{qTop}=\left({j}\in \mathrm{V},{f}\in \mathrm{V}⟼\left\{{s}\in 𝒫{f}\left[\bigcup {j}\right]|{{f}}^{-1}\left[{s}\right]\cap \bigcup {j}\in {j}\right\}\right)$
21 19 20 ovmpoga ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge \left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}\in \mathrm{V}\right)\to {J}\mathrm{qTop}{F}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
22 8 21 mpd3an3 ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in \mathrm{V}\right)\to {J}\mathrm{qTop}{F}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
23 2 3 22 syl2an ${⊢}\left({J}\in {V}\wedge {F}\in {W}\right)\to {J}\mathrm{qTop}{F}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$