ssctr

Description: The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	ssctr	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to A \subseteq_{cat} C$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to A \subseteq_{cat} B$
2		eqidd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom A = dom dom A$
3	1 2	sscfn1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to A Fn (dom dom A \times dom dom A)$
4		eqidd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom B = dom dom B$
5	1 4	sscfn2	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to B Fn (dom dom B \times dom dom B)$
6	3 5 1	ssc1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom A \subseteq dom dom B$
7		simpr	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to B \subseteq_{cat} C$
8		eqidd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom C = dom dom C$
9	7 8	sscfn2	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to C Fn (dom dom C \times dom dom C)$
10	5 9 7	ssc1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom B \subseteq dom dom C$
11	6 10	sstrd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom A \subseteq dom dom C$
12	3	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to A Fn (dom dom A \times dom dom A)$
13	1	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to A \subseteq_{cat} B$
14		simprl	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to x \in dom dom A$
15		simprr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to y \in dom dom A$
16	12 13 14 15	ssc2	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to x A y \subseteq x B y$
17	5	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to B Fn (dom dom B \times dom dom B)$
18	7	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to B \subseteq_{cat} C$
19	6	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to dom dom A \subseteq dom dom B$
20	19 14	sseldd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to x \in dom dom B$
21	19 15	sseldd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to y \in dom dom B$
22	17 18 20 21	ssc2	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to x B y \subseteq x C y$
23	16 22	sstrd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} C) \land (x \in dom dom A \land y \in dom dom A)) \to x A y \subseteq x C y$
24	23	ralrimivva	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to \forall x \in dom dom A \forall y \in dom dom A x A y \subseteq x C y$
25		sscrel	$⊢ Rel \subseteq_{cat}$
26	25	brrelex2i	$⊢ B \subseteq_{cat} C \to C \in V$
27	26	adantl	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to C \in V$
28		dmexg	$⊢ C \in V \to dom C \in V$
29		dmexg	$⊢ dom C \in V \to dom dom C \in V$
30	27 28 29	3syl	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to dom dom C \in V$
31	3 9 30	isssc	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to (A \subseteq_{cat} C \leftrightarrow (dom dom A \subseteq dom dom C \land \forall x \in dom dom A \forall y \in dom dom A x A y \subseteq x C y))$
32	11 24 31	mpbir2and	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} C) \to A \subseteq_{cat} C$

Metamath Proof Explorer

Theorem ssctr

Proof