infsubc2

Description: The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025)

		Ref	Expression
	Assertion	infsubc2	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (x \in (dom dom A \cap dom dom B), y \in (dom dom A \cap dom dom B) ⟼ (x A y) \cap (x B y)) \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		prnzg	$⊢ A \in Subcat (C) \to \{A, B\} \neq \emptyset$
2	1	adantr	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to \{A, B\} \neq \emptyset$
3		simpll	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to A \in Subcat (C)$
4		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
5	3 4	subcssc	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to A \subseteq_{cat} {Hom}_{𝑓} (C)$
6		breq1	$⊢ w = A \to (w \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow A \subseteq_{cat} {Hom}_{𝑓} (C))$
7	5 6	syl5ibrcom	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to (w = A \to w \subseteq_{cat} {Hom}_{𝑓} (C))$
8		simplr	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to B \in Subcat (C)$
9	8 4	subcssc	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to B \subseteq_{cat} {Hom}_{𝑓} (C)$
10		breq1	$⊢ w = B \to (w \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow B \subseteq_{cat} {Hom}_{𝑓} (C))$
11	9 10	syl5ibrcom	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to (w = B \to w \subseteq_{cat} {Hom}_{𝑓} (C))$
12		elpri	$⊢ w \in \{A, B\} \to (w = A \lor w = B)$
13	12	adantl	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to (w = A \lor w = B)$
14	7 11 13	mpjaod	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to w \subseteq_{cat} {Hom}_{𝑓} (C)$
15		iinfprg	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (z \in (dom A \cap dom B) ⟼ A (z) \cap B (z)) = (z \in ⋂_{w \in \{A, B\}} dom w ⟼ ⋂_{w \in \{A, B\}} w (z))$
16		eqidd	$⊢ ((A \in Subcat (C) \land B \in Subcat (C)) \land w \in \{A, B\}) \to dom dom w = dom dom w$
17		nfv	$⊢ Ⅎ w (A \in Subcat (C) \land B \in Subcat (C))$
18	2 14 15 16 17	iinfssclem1	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (z \in (dom A \cap dom B) ⟼ A (z) \cap B (z)) = (x \in ⋂_{w \in \{A, B\}} dom dom w, y \in ⋂_{w \in \{A, B\}} dom dom w ⟼ ⋂_{w \in \{A, B\}} (x w y))$
19		dmeq	$⊢ w = A \to dom w = dom A$
20	19	dmeqd	$⊢ w = A \to dom dom w = dom dom A$
21		dmeq	$⊢ w = B \to dom w = dom B$
22	21	dmeqd	$⊢ w = B \to dom dom w = dom dom B$
23	20 22	iinxprg	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to ⋂_{w \in \{A, B\}} dom dom w = dom dom A \cap dom dom B$
24		oveq	$⊢ w = A \to x w y = x A y$
25		oveq	$⊢ w = B \to x w y = x B y$
26	24 25	iinxprg	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to ⋂_{w \in \{A, B\}} (x w y) = (x A y) \cap (x B y)$
27	23 23 26	mpoeq123dv	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (x \in ⋂_{w \in \{A, B\}} dom dom w, y \in ⋂_{w \in \{A, B\}} dom dom w ⟼ ⋂_{w \in \{A, B\}} (x w y)) = (x \in (dom dom A \cap dom dom B), y \in (dom dom A \cap dom dom B) ⟼ (x A y) \cap (x B y))$
28	18 27	eqtrd	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (z \in (dom A \cap dom B) ⟼ A (z) \cap B (z)) = (x \in (dom dom A \cap dom dom B), y \in (dom dom A \cap dom dom B) ⟼ (x A y) \cap (x B y))$
29		infsubc	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (z \in (dom A \cap dom B) ⟼ A (z) \cap B (z)) \in Subcat (C)$
30	28 29	eqeltrrd	$⊢ (A \in Subcat (C) \land B \in Subcat (C)) \to (x \in (dom dom A \cap dom dom B), y \in (dom dom A \cap dom dom B) ⟼ (x A y) \cap (x B y)) \in Subcat (C)$

Metamath Proof Explorer

Theorem infsubc2

Proof