issubc

Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	issubc.h	$⊢ H = {Hom}_{𝑓} (C)$
	issubc.i	$⊢ \underset{˙}{1} = Id (C)$
	issubc.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	issubc.c	$⊢ φ \to C \in Cat$
	issubc.s	$⊢ φ \to S = dom dom J$
Assertion	issubc	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$

Proof

Step	Hyp	Ref	Expression
1		issubc.h	$⊢ H = {Hom}_{𝑓} (C)$
2		issubc.i	$⊢ \underset{˙}{1} = Id (C)$
3		issubc.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		issubc.c	$⊢ φ \to C \in Cat$
5		issubc.s	$⊢ φ \to S = dom dom J$
6		simpl	$⊢ (C \in Cat \land S = dom dom J) \to C \in Cat$
7		sscpwex	$⊢ \{j \| j \subseteq_{cat} {Hom}_{𝑓} (c)\} \in V$
8		simpl	$⊢ (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z))) \to j \subseteq_{cat} {Hom}_{𝑓} (c)$
9	8	ss2abi	$⊢ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \subseteq \{j \| j \subseteq_{cat} {Hom}_{𝑓} (c)\}$
10	7 9	ssexi	$⊢ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \in V$
11	10	csbex	$⊢ ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \in V$
12	11	a1i	$⊢ (C \in Cat \land S = dom dom J) \to ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \in V$
13		df-subc	$⊢ Subcat = (c \in Cat ⟼ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\})$
14	13	fvmpts	$⊢ (C \in Cat \land ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \in V) \to Subcat (C) = ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\}$
15	6 12 14	syl2anc	$⊢ (C \in Cat \land S = dom dom J) \to Subcat (C) = ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\}$
16	15	eleq2d	$⊢ (C \in Cat \land S = dom dom J) \to (J \in Subcat (C) \leftrightarrow J \in ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\})$
17		sbcel2	$⊢ \underset{˙}{[} C / c \underset{˙}{]} J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow J \in ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\}$
18	17	a1i	$⊢ (C \in Cat \land S = dom dom J) \to (\underset{˙}{[} C / c \underset{˙}{]} J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow J \in ⦋ C / c ⦌ \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\})$
19		elex	$⊢ J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \to J \in V$
20	19	a1i	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to (J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \to J \in V)$
21		sscrel	$⊢ Rel \subseteq_{cat}$
22	21	brrelex1i	$⊢ J \subseteq_{cat} H \to J \in V$
23	22	adantr	$⊢ (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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 J \in V$
24	23	a1i	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to ((J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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 J \in V)$
25		df-sbc	$⊢ \underset{˙}{[} J / j \underset{˙}{]} (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z))) \leftrightarrow J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\}$
26		simpr	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land J \in V) \to J \in V$
27		simpr	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to j = J$
28		simpr	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to c = C$
29	28	fveq2d	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to {Hom}_{𝑓} (c) = {Hom}_{𝑓} (C)$
30	29 1	eqtr4di	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to {Hom}_{𝑓} (c) = H$
31	30	adantr	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to {Hom}_{𝑓} (c) = H$
32	27 31	breq12d	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to (j \subseteq_{cat} {Hom}_{𝑓} (c) \leftrightarrow J \subseteq_{cat} H)$
33		vex	$⊢ j \in V$
34	33	dmex	$⊢ dom j \in V$
35	34	dmex	$⊢ dom dom j \in V$
36	35	a1i	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to dom dom j \in V$
37	27	dmeqd	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to dom j = dom J$
38	37	dmeqd	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to dom dom j = dom dom J$
39		simpllr	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to S = dom dom J$
40	38 39	eqtr4d	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to dom dom j = S$
41		simpr	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to s = S$
42		simpllr	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to c = C$
43	42	fveq2d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to Id (c) = Id (C)$
44	43 2	eqtr4di	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to Id (c) = \underset{˙}{1}$
45	44	fveq1d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to Id (c) (x) = \underset{˙}{1} (x)$
46		simplr	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to j = J$
47	46	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to x j x = x J x$
48	45 47	eleq12d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (Id (c) (x) \in (x j x) \leftrightarrow \underset{˙}{1} (x) \in (x J x))$
49	46	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to x j y = x J y$
50	46	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to y j z = y J z$
51	42	fveq2d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to comp (c) = comp (C)$
52	51 3	eqtr4di	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to comp (c) = \underset{˙}{\cdot}$
53	52	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to ⟨x, y⟩ comp (c) z = ⟨x, y⟩ \underset{˙}{\cdot} z$
54	53	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to g (⟨x, y⟩ comp (c) z) f = g (⟨x, y⟩ \underset{˙}{\cdot} z) f$
55	46	oveqd	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to x j z = x J z$
56	54 55	eleq12d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z))$
57	50 56	raleqbidv	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (\forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z))$
58	49 57	raleqbidv	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (\forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z))$
59	41 58	raleqbidv	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (\forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \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))$
60	41 59	raleqbidv	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \to (\forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \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))$
61	48 60	anbi12d	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \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⟩ comp (c) z) f \in (x j z)) \leftrightarrow (\underset{˙}{1} (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)))$
62	41 61	raleqbidv	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \land s = S) \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⟩ comp (c) z) f \in (x j z)) \leftrightarrow \forall x \in S (\underset{˙}{1} (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)))$
63	36 40 62	sbcied2	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to (\underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)) \leftrightarrow \forall x \in S (\underset{˙}{1} (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)))$
64	32 63	anbi12d	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land j = J) \to ((j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z))) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
65	64	adantlr	$⊢ ((((C \in Cat \land S = dom dom J) \land c = C) \land J \in V) \land j = J) \to ((j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z))) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
66	26 65	sbcied	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land J \in V) \to (\underset{˙}{[} J / j \underset{˙}{]} (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z))) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
67	25 66	bitr3id	$⊢ (((C \in Cat \land S = dom dom J) \land c = C) \land J \in V) \to (J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
68	67	ex	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to (J \in V \to (J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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)))))$
69	20 24 68	pm5.21ndd	$⊢ ((C \in Cat \land S = dom dom J) \land c = C) \to (J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
70	6 69	sbcied	$⊢ (C \in Cat \land S = dom dom J) \to (\underset{˙}{[} C / c \underset{˙}{]} J \in \{j \| (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom j / s \underset{˙}{]} \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⟩ comp (c) z) f \in (x j z)))\} \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
71	16 18 70	3bitr2d	$⊢ (C \in Cat \land S = dom dom J) \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$
72	4 5 71	syl2anc	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (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))))$

Metamath Proof Explorer

Theorem issubc

Proof