Metamath Proof Explorer

Theorem qtopcld

Description: The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion qtopcld 
|- ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( Clsd ` ( J qTop F ) ) <-> ( A C_ Y /\ ( `' F " A ) e. ( Clsd ` J ) ) ) )

Proof

Step Hyp Ref Expression
1 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )
2 topontop 
 |-  ( ( J qTop F ) e. ( TopOn ` Y ) -> ( J qTop F ) e. Top )
3 eqid 
 |-  U. ( J qTop F ) = U. ( J qTop F )
4 3 iscld 
 |-  ( ( J qTop F ) e. Top -> ( A e. ( Clsd ` ( J qTop F ) ) <-> ( A C_ U. ( J qTop F ) /\ ( U. ( J qTop F ) \ A ) e. ( J qTop F ) ) ) )
5 1 2 4 3syl 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( Clsd ` ( J qTop F ) ) <-> ( A C_ U. ( J qTop F ) /\ ( U. ( J qTop F ) \ A ) e. ( J qTop F ) ) ) )
6 toponuni 
 |-  ( ( J qTop F ) e. ( TopOn ` Y ) -> Y = U. ( J qTop F ) )
7 1 6 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )
8 7 sseq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A C_ Y <-> A C_ U. ( J qTop F ) ) )
9 7 difeq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( Y \ A ) = ( U. ( J qTop F ) \ A ) )
10 9 eleq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( ( Y \ A ) e. ( J qTop F ) <-> ( U. ( J qTop F ) \ A ) e. ( J qTop F ) ) )
11 8 10 anbi12d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( ( A C_ Y /\ ( Y \ A ) e. ( J qTop F ) ) <-> ( A C_ U. ( J qTop F ) /\ ( U. ( J qTop F ) \ A ) e. ( J qTop F ) ) ) )
12 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( ( Y \ A ) e. ( J qTop F ) <-> ( ( Y \ A ) C_ Y /\ ( `' F " ( Y \ A ) ) e. J ) ) )
13 12 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( Y \ A ) e. ( J qTop F ) <-> ( ( Y \ A ) C_ Y /\ ( `' F " ( Y \ A ) ) e. J ) ) )
14 difss 
 |-  ( Y \ A ) C_ Y
15 14 biantrur 
 |-  ( ( `' F " ( Y \ A ) ) e. J <-> ( ( Y \ A ) C_ Y /\ ( `' F " ( Y \ A ) ) e. J ) )
16 fofun 
 |-  ( F : X -onto-> Y -> Fun F )
17 16 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> Fun F )
18 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
19 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( Y \ A ) ) = ( ( `' F " Y ) \ ( `' F " A ) ) )
20 17 18 19 3syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " ( Y \ A ) ) = ( ( `' F " Y ) \ ( `' F " A ) ) )
21 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
22 fimacnv 
 |-  ( F : X --> Y -> ( `' F " Y ) = X )
23 21 22 syl 
 |-  ( F : X -onto-> Y -> ( `' F " Y ) = X )
24 23 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " Y ) = X )
25 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
26 25 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> X = U. J )
27 24 26 eqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " Y ) = U. J )
28 27 difeq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( `' F " Y ) \ ( `' F " A ) ) = ( U. J \ ( `' F " A ) ) )
29 20 28 eqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " ( Y \ A ) ) = ( U. J \ ( `' F " A ) ) )
30 29 eleq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( `' F " ( Y \ A ) ) e. J <-> ( U. J \ ( `' F " A ) ) e. J ) )
31 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
32 31 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> J e. Top )
33 cnvimass 
 |-  ( `' F " A ) C_ dom F
34 fofn 
 |-  ( F : X -onto-> Y -> F Fn X )
35 34 fndmd 
 |-  ( F : X -onto-> Y -> dom F = X )
36 35 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> dom F = X )
37 33 36 sseqtrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " A ) C_ X )
38 37 26 sseqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( `' F " A ) C_ U. J )
39 eqid 
 |-  U. J = U. J
40 39 iscld2 
 |-  ( ( J e. Top /\ ( `' F " A ) C_ U. J ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) )
41 32 38 40 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) )
42 30 41 bitr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( `' F " ( Y \ A ) ) e. J <-> ( `' F " A ) e. ( Clsd ` J ) ) )
43 15 42 bitr3id 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( ( Y \ A ) C_ Y /\ ( `' F " ( Y \ A ) ) e. J ) <-> ( `' F " A ) e. ( Clsd ` J ) ) )
44 13 43 bitrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) /\ A C_ Y ) -> ( ( Y \ A ) e. ( J qTop F ) <-> ( `' F " A ) e. ( Clsd ` J ) ) )
45 44 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( ( A C_ Y /\ ( Y \ A ) e. ( J qTop F ) ) <-> ( A C_ Y /\ ( `' F " A ) e. ( Clsd ` J ) ) ) )
46 5 11 45 3bitr2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( Clsd ` ( J qTop F ) ) <-> ( A C_ Y /\ ( `' F " A ) e. ( Clsd ` J ) ) ) )