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 34 fndmd ⊢ F : X ⟶ onto Y → dom ⁡ F = X
36 35 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → dom ⁡ F = X
37 33 36 sseqtrid ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → F -1 A ⊆ X
38 37 26 sseqtrd ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → F -1 A ⊆ ⋃ J
39 eqid ⊢ ⋃ J = ⋃ J
40 39 iscld2 ⊢ J ∈ Top ∧ F -1 A ⊆ ⋃ J → F -1 A ∈ Clsd ⁡ J ↔ ⋃ J ∖ F -1 A ∈ J
41 32 38 40 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → F -1 A ∈ Clsd ⁡ J ↔ ⋃ J ∖ F -1 A ∈ J
42 30 41 bitr4d ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → F -1 Y ∖ A ∈ J ↔ F -1 A ∈ Clsd ⁡ J
43 15 42 bitr3id ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → Y ∖ A ⊆ Y ∧ F -1 Y ∖ A ∈ J ↔ F -1 A ∈ Clsd ⁡ J
44 13 43 bitrd ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y ∧ A ⊆ Y → Y ∖ A ∈ J qTop F ↔ F -1 A ∈ Clsd ⁡ J
45 44 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → A ⊆ Y ∧ Y ∖ A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ Clsd ⁡ J
46 5 11 45 3bitr2d ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto Y → A ∈ Clsd ⁡ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ Clsd ⁡ J