This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
2 topontop ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
3 eqid ⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
4 3 iscld ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ Top → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ ∪ ( 𝐽 qTop 𝐹 ) ∧ ( ∪ ( 𝐽 qTop 𝐹 ) ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
5 1 2 4 3syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ ∪ ( 𝐽 qTop 𝐹 ) ∧ ( ∪ ( 𝐽 qTop 𝐹 ) ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
6 toponuni ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
7 1 6 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
8 7 sseq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ⊆ 𝑌 ↔ 𝐴 ⊆ ∪ ( 𝐽 qTop 𝐹 ) ) )
9 7 difeq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑌 ∖ 𝐴 ) = ( ∪ ( 𝐽 qTop 𝐹 ) ∖ 𝐴 ) )
10 9 eleq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ∪ ( 𝐽 qTop 𝐹 ) ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) )
11 8 10 anbi12d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝐴 ⊆ 𝑌 ∧ ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ ∪ ( 𝐽 qTop 𝐹 ) ∧ ( ∪ ( 𝐽 qTop 𝐹 ) ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
12 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ) ) )
13 12 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ) ) )
14 difss ⊢ ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌
15 14 biantrur ⊢ ( ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ↔ ( ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ) )
16 fofun ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → Fun 𝐹 )
17 16 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → Fun 𝐹 )
18 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
19 imadif ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
20 17 18 19 3syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
21 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
22 fimacnv ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = 𝑋 )
23 21 22 syl ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = 𝑋 )
24 23 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝑌 ) = 𝑋 )
25 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
26 25 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝑋 = ∪ 𝐽 )
27 24 26 eqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
28 27 difeq1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
29 20 28 eqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
30 29 eleq1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 ) )
31 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
32 31 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐽 ∈ Top )
33 cnvimass ⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
34 fofn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 Fn 𝑋 )
35 34 fndmd ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → dom 𝐹 = 𝑋 )
36 35 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → dom 𝐹 = 𝑋 )
37 33 36 sseqtrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝑋 )
38 37 26 sseqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ ∪ 𝐽 )
39 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
40 39 iscld2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝐴 ) ⊆ ∪ 𝐽 ) → ( ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 ) )
41 32 38 40 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 ) )
42 30 41 bitr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) )
43 15 42 bitr3id ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝐴 ) ) ∈ 𝐽 ) ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) )
44 13 43 bitrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) )
45 44 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝐴 ⊆ 𝑌 ∧ ( 𝑌 ∖ 𝐴 ) ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
46 5 11 45 3bitr2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐴 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )