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 𝐾 ) ) )