Metamath Proof Explorer

Theorem qtopcn

Description: Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion qtopcn ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( 𝐺 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ ( ◡ 𝐺 “ 𝑥 ) ⊆ dom 𝐺
2 simplrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝐺 : 𝑌 ⟶ 𝑍 )
3 1 2 fssdm ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐺 “ 𝑥 ) ⊆ 𝑌 )
4 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 simplrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝐹 : 𝑋 –onto→ 𝑌 )
6 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( ◡ 𝐺 “ 𝑥 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 ) ) )
7 4 5 6 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( ◡ 𝐺 “ 𝑥 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 ) ) )
8 3 7 mpbirand ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 ) )
9 cnvco ⊢ ◡ ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐺 )
10 9 imaeq1i ⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) = ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑥 )
11 imaco ⊢ ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) )
12 10 11 eqtri ⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) )
13 12 eleq1i ⊢ ( ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 )
14 8 13 bitr4di ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) )
15 14 ralbidva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) )
16 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → 𝐺 : 𝑌 ⟶ 𝑍 )
17 16 biantrurd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐺 : 𝑌 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
18 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
19 18 ad2antrl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
20 fco ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑍 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 )
21 16 19 20 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 )
22 21 biantrurd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) ) )
23 15 17 22 3bitr3d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( ( 𝐺 : 𝑌 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) ) )
24 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
25 24 ad2ant2r ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
26 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑍 ) )
27 iscn ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) → ( 𝐺 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( 𝐺 : 𝑌 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
28 25 26 27 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( 𝐺 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( 𝐺 : 𝑌 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐺 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
29 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) ) )
30 29 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝑋 ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) ) )
31 23 28 30 3bitr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐺 : 𝑌 ⟶ 𝑍 ) ) → ( 𝐺 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ) )