subsubc

Description: A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Hypothesis	subsubc.d	$⊢ D = C ↾_{cat} H$
	Assertion	subsubc	$⊢ H \in Subcat (C) \to (J \in Subcat (D) \leftrightarrow (J \in Subcat (C) \land J \subseteq_{cat} H))$

Proof

Step	Hyp	Ref	Expression
1		subsubc.d	$⊢ D = C ↾_{cat} H$
2		id	$⊢ J \in Subcat (D) \to J \in Subcat (D)$
3		eqid	$⊢ {Hom}_{𝑓} (D) = {Hom}_{𝑓} (D)$
4	2 3	subcssc	$⊢ J \in Subcat (D) \to J \subseteq_{cat} {Hom}_{𝑓} (D)$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		subcrcl	$⊢ H \in Subcat (C) \to C \in Cat$
7		id	$⊢ H \in Subcat (C) \to H \in Subcat (C)$
8		eqidd	$⊢ H \in Subcat (C) \to dom dom H = dom dom H$
9	7 8	subcfn	$⊢ H \in Subcat (C) \to H Fn (dom dom H \times dom dom H)$
10	7 9 5	subcss1	$⊢ H \in Subcat (C) \to dom dom H \subseteq {Base}_{C}$
11	1 5 6 9 10	reschomf	$⊢ H \in Subcat (C) \to H = {Hom}_{𝑓} (D)$
12	11	breq2d	$⊢ H \in Subcat (C) \to (J \subseteq_{cat} H \leftrightarrow J \subseteq_{cat} {Hom}_{𝑓} (D))$
13	4 12	syl5ibr	$⊢ H \in Subcat (C) \to (J \in Subcat (D) \to J \subseteq_{cat} H)$
14	13	pm4.71rd	$⊢ H \in Subcat (C) \to (J \in Subcat (D) \leftrightarrow (J \subseteq_{cat} H \land J \in Subcat (D)))$
15		simpr	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to J \subseteq_{cat} H$
16		simpl	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to H \in Subcat (C)$
17		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
18	16 17	subcssc	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to H \subseteq_{cat} {Hom}_{𝑓} (C)$
19		ssctr	$⊢ (J \subseteq_{cat} H \land H \subseteq_{cat} {Hom}_{𝑓} (C)) \to J \subseteq_{cat} {Hom}_{𝑓} (C)$
20	15 18 19	syl2anc	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to J \subseteq_{cat} {Hom}_{𝑓} (C)$
21	12	biimpa	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to J \subseteq_{cat} {Hom}_{𝑓} (D)$
22	20 21	2thd	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (J \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow J \subseteq_{cat} {Hom}_{𝑓} (D))$
23	16	adantr	$⊢ ((H \in Subcat (C) \land J \subseteq_{cat} H) \land x \in dom dom J) \to H \in Subcat (C)$
24	9	adantr	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to H Fn (dom dom H \times dom dom H)$
25	24	adantr	$⊢ ((H \in Subcat (C) \land J \subseteq_{cat} H) \land x \in dom dom J) \to H Fn (dom dom H \times dom dom H)$
26		eqid	$⊢ Id (C) = Id (C)$
27		eqidd	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to dom dom J = dom dom J$
28	15 27	sscfn1	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to J Fn (dom dom J \times dom dom J)$
29	28 24 15	ssc1	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to dom dom J \subseteq dom dom H$
30	29	sselda	$⊢ ((H \in Subcat (C) \land J \subseteq_{cat} H) \land x \in dom dom J) \to x \in dom dom H$
31	1 23 25 26 30	subcid	$⊢ ((H \in Subcat (C) \land J \subseteq_{cat} H) \land x \in dom dom J) \to Id (C) (x) = Id (D) (x)$
32	31	eleq1d	$⊢ ((H \in Subcat (C) \land J \subseteq_{cat} H) \land x \in dom dom J) \to (Id (C) (x) \in (x J x) \leftrightarrow Id (D) (x) \in (x J x))$
33	32	ralbidva	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (\forall x \in dom dom J Id (C) (x) \in (x J x) \leftrightarrow \forall x \in dom dom J Id (D) (x) \in (x J x))$
34	1	oveq1i	$⊢ D ↾_{cat} J = (C ↾_{cat} H) ↾_{cat} J$
35	6	adantr	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to C \in Cat$
36		dmexg	$⊢ H \in Subcat (C) \to dom H \in V$
37	36	dmexd	$⊢ H \in Subcat (C) \to dom dom H \in V$
38	37	adantr	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to dom dom H \in V$
39	35 24 28 38 29	rescabs	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (C ↾_{cat} H) ↾_{cat} J = C ↾_{cat} J$
40	34 39	eqtr2id	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to C ↾_{cat} J = D ↾_{cat} J$
41	40	eleq1d	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (C ↾_{cat} J \in Cat \leftrightarrow D ↾_{cat} J \in Cat)$
42	22 33 41	3anbi123d	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to ((J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in dom dom J Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (D) \land \forall x \in dom dom J Id (D) (x) \in (x J x) \land D ↾_{cat} J \in Cat))$
43		eqid	$⊢ C ↾_{cat} J = C ↾_{cat} J$
44	17 26 43 35 28	issubc3	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in dom dom J Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
45		eqid	$⊢ Id (D) = Id (D)$
46		eqid	$⊢ D ↾_{cat} J = D ↾_{cat} J$
47	1 7	subccat	$⊢ H \in Subcat (C) \to D \in Cat$
48	47	adantr	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to D \in Cat$
49	3 45 46 48 28	issubc3	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (J \in Subcat (D) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (D) \land \forall x \in dom dom J Id (D) (x) \in (x J x) \land D ↾_{cat} J \in Cat))$
50	42 44 49	3bitr4rd	$⊢ (H \in Subcat (C) \land J \subseteq_{cat} H) \to (J \in Subcat (D) \leftrightarrow J \in Subcat (C))$
51	50	pm5.32da	$⊢ H \in Subcat (C) \to ((J \subseteq_{cat} H \land J \in Subcat (D)) \leftrightarrow (J \subseteq_{cat} H \land J \in Subcat (C)))$
52	14 51	bitrd	$⊢ H \in Subcat (C) \to (J \in Subcat (D) \leftrightarrow (J \subseteq_{cat} H \land J \in Subcat (C)))$
53	52	biancomd	$⊢ H \in Subcat (C) \to (J \in Subcat (D) \leftrightarrow (J \in Subcat (C) \land J \subseteq_{cat} H))$

Metamath Proof Explorer

Theorem subsubc

Proof