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 TopOn X F : X onto Y A Clsd J qTop F A Y F -1 A Clsd J

Proof

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