subccocl

Description: A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subcidcl.j	$⊢ φ \to J \in Subcat (C)$
	subcidcl.2	$⊢ φ \to J Fn (S \times S)$
	subcidcl.x	$⊢ φ \to X \in S$
	subccocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	subccocl.y	$⊢ φ \to Y \in S$
	subccocl.z	$⊢ φ \to Z \in S$
	subccocl.f	$⊢ φ \to F \in (X J Y)$
	subccocl.g	$⊢ φ \to G \in (Y J Z)$
Assertion	subccocl	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z)$

Proof

Step	Hyp	Ref	Expression
1		subcidcl.j	$⊢ φ \to J \in Subcat (C)$
2		subcidcl.2	$⊢ φ \to J Fn (S \times S)$
3		subcidcl.x	$⊢ φ \to X \in S$
4		subccocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
5		subccocl.y	$⊢ φ \to Y \in S$
6		subccocl.z	$⊢ φ \to Z \in S$
7		subccocl.f	$⊢ φ \to F \in (X J Y)$
8		subccocl.g	$⊢ φ \to G \in (Y J Z)$
9		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11		subcrcl	$⊢ J \in Subcat (C) \to C \in Cat$
12	1 11	syl	$⊢ φ \to C \in Cat$
13	9 10 4 12 2	issubc2	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z))))$
14	1 13	mpbid	$⊢ φ \to (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)))$
15	14	simprd	$⊢ φ \to \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z))$
16	5	adantr	$⊢ (φ \land x = X) \to Y \in S$
17	6	ad2antrr	$⊢ ((φ \land x = X) \land y = Y) \to Z \in S$
18	7	ad3antrrr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (X J Y)$
19		simpllr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x = X$
20		simplr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to y = Y$
21	19 20	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x J y = X J Y$
22	18 21	eleqtrrd	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (x J y)$
23	8	ad4antr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to G \in (Y J Z)$
24		simpllr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to y = Y$
25		simplr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to z = Z$
26	24 25	oveq12d	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to y J z = Y J Z$
27	23 26	eleqtrrd	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to G \in (y J z)$
28		simp-5r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to x = X$
29		simp-4r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to y = Y$
30	28 29	opeq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to ⟨x, y⟩ = ⟨X, Y⟩$
31		simpllr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to z = Z$
32	30 31	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$
33		simpr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to g = G$
34		simplr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to f = F$
35	32 33 34	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$
36	28 31	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to x J z = X J Z$
37	35 36	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 J z) \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
38	27 37	rspcdv	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to (\forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
39	22 38	rspcimdv	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to (\forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
40	17 39	rspcimdv	$⊢ ((φ \land x = X) \land y = Y) \to (\forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
41	16 40	rspcimdv	$⊢ (φ \land x = X) \to (\forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
42	41	adantld	$⊢ (φ \land x = X) \to ((Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
43	3 42	rspcimdv	$⊢ φ \to (\forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z))$
44	15 43	mpd	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X J Z)$

Metamath Proof Explorer

Theorem subccocl

Proof