catcocl

Description: Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	catcocl.b	$⊢ B = {Base}_{C}$
	catcocl.h	$⊢ H = Hom (C)$
	catcocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	catcocl.c	$⊢ φ \to C \in Cat$
	catcocl.x	$⊢ φ \to X \in B$
	catcocl.y	$⊢ φ \to Y \in B$
	catcocl.z	$⊢ φ \to Z \in B$
	catcocl.f	$⊢ φ \to F \in (X H Y)$
	catcocl.g	$⊢ φ \to G \in (Y H Z)$
Assertion	catcocl	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z)$

Proof

Step	Hyp	Ref	Expression
1		catcocl.b	$⊢ B = {Base}_{C}$
2		catcocl.h	$⊢ H = Hom (C)$
3		catcocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		catcocl.c	$⊢ φ \to C \in Cat$
5		catcocl.x	$⊢ φ \to X \in B$
6		catcocl.y	$⊢ φ \to Y \in B$
7		catcocl.z	$⊢ φ \to Z \in B$
8		catcocl.f	$⊢ φ \to F \in (X H Y)$
9		catcocl.g	$⊢ φ \to G \in (Y H Z)$
10	1 2 3	iscat	$⊢ C \in Cat \to (C \in Cat \leftrightarrow \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))))$
11	10	ibi	$⊢ C \in Cat \to \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
12		simpl	$⊢ (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
13	12	2ralimi	$⊢ \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
14	13	2ralimi	$⊢ \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
15	14	adantl	$⊢ (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \to \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
16	15	ralimi	$⊢ \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall v \in (z H w) (v (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = v (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
17	4 11 16	3syl	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
18	6	adantr	$⊢ (φ \land x = X) \to Y \in B$
19	7	ad2antrr	$⊢ ((φ \land x = X) \land y = Y) \to Z \in B$
20	8	ad3antrrr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (X H Y)$
21		simpllr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x = X$
22		simplr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to y = Y$
23	21 22	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x H y = X H Y$
24	20 23	eleqtrrd	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (x H y)$
25	9	ad3antrrr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to G \in (Y H Z)$
26		simpr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to z = Z$
27	22 26	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to y H z = Y H Z$
28	25 27	eleqtrrd	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to G \in (y H z)$
29	28	adantr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to G \in (y H z)$
30		simp-5r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to x = X$
31		simp-4r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to y = Y$
32	30 31	opeq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to ⟨x, y⟩ = ⟨X, Y⟩$
33		simpllr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to z = Z$
34	32 33	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨X, Y⟩ \underset{˙}{\cdot} Z$
35		simpr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to g = G$
36		simplr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to f = F$
37	34 35 36	oveq123d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
38	30 33	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to x H z = X H Z$
39	37 38	eleq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
40	29 39	rspcdv	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to (\forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
41	24 40	rspcimdv	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to (\forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
42	19 41	rspcimdv	$⊢ ((φ \land x = X) \land y = Y) \to (\forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
43	18 42	rspcimdv	$⊢ (φ \land x = X) \to (\forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
44	5 43	rspcimdv	$⊢ φ \to (\forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
45	17 44	mpd	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z)$

Metamath Proof Explorer

Theorem catcocl

Proof