setcco

Description: Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcbas.c	$⊢ C = SetCat (U)$
	setcbas.u	$⊢ φ \to U \in V$
	setcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	setcco.x	$⊢ φ \to X \in U$
	setcco.y	$⊢ φ \to Y \in U$
	setcco.z	$⊢ φ \to Z \in U$
	setcco.f	$⊢ φ \to F : X ⟶ Y$
	setcco.g	$⊢ φ \to G : Y ⟶ Z$
Assertion	setcco	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ F$

Proof

Step	Hyp	Ref	Expression
1		setcbas.c	$⊢ C = SetCat (U)$
2		setcbas.u	$⊢ φ \to U \in V$
3		setcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		setcco.x	$⊢ φ \to X \in U$
5		setcco.y	$⊢ φ \to Y \in U$
6		setcco.z	$⊢ φ \to Z \in U$
7		setcco.f	$⊢ φ \to F : X ⟶ Y$
8		setcco.g	$⊢ φ \to G : Y ⟶ Z$
9	1 2 3	setccofval	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
10		simprr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to z = Z$
11		simprl	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to v = ⟨X, Y⟩$
12	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = 2^{nd} (⟨X, Y⟩)$
13		op2ndg	$⊢ (X \in U \land Y \in U) \to 2^{nd} (⟨X, Y⟩) = Y$
14	4 5 13	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
15	14	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
16	12 15	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = Y$
17	10 16	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to z^{2^{nd} (v)} = Z^{Y}$
18	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) = 1^{st} (⟨X, Y⟩)$
19		op1stg	$⊢ (X \in U \land Y \in U) \to 1^{st} (⟨X, Y⟩) = X$
20	4 5 19	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
21	20	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (⟨X, Y⟩) = X$
22	18 21	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) = X$
23	16 22	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {2^{nd} (v)}^{1^{st} (v)} = Y^{X}$
24		eqidd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to g \circ f = g \circ f$
25	17 23 24	mpoeq123dv	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f) = (g \in (Z^{Y}), f \in (Y^{X}) ⟼ g \circ f)$
26	4 5	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (U \times U)$
27		ovex	$⊢ Z^{Y} \in V$
28		ovex	$⊢ Y^{X} \in V$
29	27 28	mpoex	$⊢ (g \in (Z^{Y}), f \in (Y^{X}) ⟼ g \circ f) \in V$
30	29	a1i	$⊢ φ \to (g \in (Z^{Y}), f \in (Y^{X}) ⟼ g \circ f) \in V$
31	9 25 26 6 30	ovmpod	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = (g \in (Z^{Y}), f \in (Y^{X}) ⟼ g \circ f)$
32		simprl	$⊢ (φ \land (g = G \land f = F)) \to g = G$
33		simprr	$⊢ (φ \land (g = G \land f = F)) \to f = F$
34	32 33	coeq12d	$⊢ (φ \land (g = G \land f = F)) \to g \circ f = G \circ F$
35	6 5	elmapd	$⊢ φ \to (G \in (Z^{Y}) \leftrightarrow G : Y ⟶ Z)$
36	8 35	mpbird	$⊢ φ \to G \in (Z^{Y})$
37	5 4	elmapd	$⊢ φ \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
38	7 37	mpbird	$⊢ φ \to F \in (Y^{X})$
39		coexg	$⊢ (G \in (Z^{Y}) \land F \in (Y^{X})) \to G \circ F \in V$
40	36 38 39	syl2anc	$⊢ φ \to G \circ F \in V$
41	31 34 36 38 40	ovmpod	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ F$

Metamath Proof Explorer

Theorem setcco

Proof