ssceq

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to A \subseteq_{cat} B$
2		eqidd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom A = dom dom A$
3	1 2	sscfn1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to A Fn (dom dom A \times dom dom A)$
4		simpr	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to B \subseteq_{cat} A$
5		eqidd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom B = dom dom B$
6	4 5	sscfn1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to B Fn (dom dom B \times dom dom B)$
7	3 6 1	ssc1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom A \subseteq dom dom B$
8	6 3 4	ssc1	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom B \subseteq dom dom A$
9	7 8	eqssd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom A = dom dom B$
10	9	sqxpeqd	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to dom dom A \times dom dom A = dom dom B \times dom dom B$
11	3	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to A Fn (dom dom A \times dom dom A)$
12	1	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to A \subseteq_{cat} B$
13		simprl	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to x \in dom dom A$
14		simprr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to y \in dom dom A$
15	11 12 13 14	ssc2	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to x A y \subseteq x B y$
16	6	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to B Fn (dom dom B \times dom dom B)$
17	4	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to B \subseteq_{cat} A$
18	7	adantr	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to dom dom A \subseteq dom dom B$
19	18 13	sseldd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to x \in dom dom B$
20	18 14	sseldd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to y \in dom dom B$
21	16 17 19 20	ssc2	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to x B y \subseteq x A y$
22	15 21	eqssd	$⊢ ((A \subseteq_{cat} B \land B \subseteq_{cat} A) \land (x \in dom dom A \land y \in dom dom A)) \to x A y = x B y$
23	22	ralrimivva	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to \forall x \in dom dom A \forall y \in dom dom A x A y = x B y$
24		eqfnov	$⊢ (A Fn (dom dom A \times dom dom A) \land B Fn (dom dom B \times dom dom B)) \to (A = B \leftrightarrow (dom dom A \times dom dom A = dom dom B \times dom dom B \land \forall x \in dom dom A \forall y \in dom dom A x A y = x B y))$
25	3 6 24	syl2anc	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to (A = B \leftrightarrow (dom dom A \times dom dom A = dom dom B \times dom dom B \land \forall x \in dom dom A \forall y \in dom dom A x A y = x B y))$
26	10 23 25	mpbir2and	$⊢ (A \subseteq_{cat} B \land B \subseteq_{cat} A) \to A = B$

Metamath Proof Explorer

Theorem ssceq

Proof