qtopcn

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

		Ref	Expression
	Assertion	qtopcn	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (G \in ((J qTop F) Cn K) \leftrightarrow G \circ F \in (J Cn K))$

Proof

Step	Hyp	Ref	Expression
1		cnvimass	$⊢ G^{-1} [x] \subseteq dom G$
2		simplrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to G : Y ⟶ Z$
3	1 2	fssdm	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to G^{-1} [x] \subseteq Y$
4		simplll	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to J \in TopOn (X)$
5		simplrl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to F : X \underset{onto}{⟶} Y$
6		elqtop3	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to (G^{-1} [x] \in (J qTop F) \leftrightarrow (G^{-1} [x] \subseteq Y \land F^{-1} [G^{-1} [x]] \in J))$
7	4 5 6	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to (G^{-1} [x] \in (J qTop F) \leftrightarrow (G^{-1} [x] \subseteq Y \land F^{-1} [G^{-1} [x]] \in J))$
8	3 7	mpbirand	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to (G^{-1} [x] \in (J qTop F) \leftrightarrow F^{-1} [G^{-1} [x]] \in J)$
9		cnvco	$⊢ {(G \circ F)}^{-1} = F^{-1} \circ G^{-1}$
10	9	imaeq1i	$⊢ {(G \circ F)}^{-1} [x] = (F^{-1} \circ G^{-1}) [x]$
11		imaco	$⊢ (F^{-1} \circ G^{-1}) [x] = F^{-1} [G^{-1} [x]]$
12	10 11	eqtri	$⊢ {(G \circ F)}^{-1} [x] = F^{-1} [G^{-1} [x]]$
13	12	eleq1i	$⊢ {(G \circ F)}^{-1} [x] \in J \leftrightarrow F^{-1} [G^{-1} [x]] \in J$
14	8 13	bitr4di	$⊢ (((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \land x \in K) \to (G^{-1} [x] \in (J qTop F) \leftrightarrow {(G \circ F)}^{-1} [x] \in J)$
15	14	ralbidva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (\forall x \in K G^{-1} [x] \in (J qTop F) \leftrightarrow \forall x \in K {(G \circ F)}^{-1} [x] \in J)$
16		simprr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to G : Y ⟶ Z$
17	16	biantrurd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (\forall x \in K G^{-1} [x] \in (J qTop F) \leftrightarrow (G : Y ⟶ Z \land \forall x \in K G^{-1} [x] \in (J qTop F)))$
18		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
19	18	ad2antrl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to F : X ⟶ Y$
20		fco	$⊢ (G : Y ⟶ Z \land F : X ⟶ Y) \to (G \circ F) : X ⟶ Z$
21	16 19 20	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (G \circ F) : X ⟶ Z$
22	21	biantrurd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (\forall x \in K {(G \circ F)}^{-1} [x] \in J \leftrightarrow ((G \circ F) : X ⟶ Z \land \forall x \in K {(G \circ F)}^{-1} [x] \in J))$
23	15 17 22	3bitr3d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to ((G : Y ⟶ Z \land \forall x \in K G^{-1} [x] \in (J qTop F)) \leftrightarrow ((G \circ F) : X ⟶ Z \land \forall x \in K {(G \circ F)}^{-1} [x] \in J))$
24		qtoptopon	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to J qTop F \in TopOn (Y)$
25	24	ad2ant2r	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to J qTop F \in TopOn (Y)$
26		simplr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to K \in TopOn (Z)$
27		iscn	$⊢ (J qTop F \in TopOn (Y) \land K \in TopOn (Z)) \to (G \in ((J qTop F) Cn K) \leftrightarrow (G : Y ⟶ Z \land \forall x \in K G^{-1} [x] \in (J qTop F)))$
28	25 26 27	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (G \in ((J qTop F) Cn K) \leftrightarrow (G : Y ⟶ Z \land \forall x \in K G^{-1} [x] \in (J qTop F)))$
29		iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (Z)) \to (G \circ F \in (J Cn K) \leftrightarrow ((G \circ F) : X ⟶ Z \land \forall x \in K {(G \circ F)}^{-1} [x] \in J))$
30	29	adantr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (G \circ F \in (J Cn K) \leftrightarrow ((G \circ F) : X ⟶ Z \land \forall x \in K {(G \circ F)}^{-1} [x] \in J))$
31	23 28 30	3bitr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Z)) \land (F : X \underset{onto}{⟶} Y \land G : Y ⟶ Z)) \to (G \in ((J qTop F) Cn K) \leftrightarrow G \circ F \in (J Cn K))$

Metamath Proof Explorer

Theorem qtopcn

Proof