infsubc2d

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

	Ref	Expression
Hypotheses	infsubc2d.1	$⊢ φ \to H Fn (S \times S)$
	infsubc2d.2	$⊢ φ \to J Fn (T \times T)$
	infsubc2d.3	$⊢ φ \to H \in Subcat (C)$
	infsubc2d.4	$⊢ φ \to J \in Subcat (C)$
Assertion	infsubc2d	$⊢ φ \to (x \in (S \cap T), y \in (S \cap T) ⟼ (x H y) \cap (x J y)) \in Subcat (C)$

Step	Hyp	Ref	Expression
1		infsubc2d.1	$⊢ φ \to H Fn (S \times S)$
2		infsubc2d.2	$⊢ φ \to J Fn (T \times T)$
3		infsubc2d.3	$⊢ φ \to H \in Subcat (C)$
4		infsubc2d.4	$⊢ φ \to J \in Subcat (C)$
5	1	fndmd	$⊢ φ \to dom H = S \times S$
6	5	dmeqd	$⊢ φ \to dom dom H = dom (S \times S)$
7		dmxpid	$⊢ dom (S \times S) = S$
8	6 7	eqtrdi	$⊢ φ \to dom dom H = S$
9	2	fndmd	$⊢ φ \to dom J = T \times T$
10	9	dmeqd	$⊢ φ \to dom dom J = dom (T \times T)$
11		dmxpid	$⊢ dom (T \times T) = T$
12	10 11	eqtrdi	$⊢ φ \to dom dom J = T$
13	8 12	ineq12d	$⊢ φ \to dom dom H \cap dom dom J = S \cap T$
14		mpoeq12	$⊢ (dom dom H \cap dom dom J = S \cap T \land dom dom H \cap dom dom J = S \cap T) \to (x \in (dom dom H \cap dom dom J), y \in (dom dom H \cap dom dom J) ⟼ (x H y) \cap (x J y)) = (x \in (S \cap T), y \in (S \cap T) ⟼ (x H y) \cap (x J y))$
15	13 13 14	syl2anc	$⊢ φ \to (x \in (dom dom H \cap dom dom J), y \in (dom dom H \cap dom dom J) ⟼ (x H y) \cap (x J y)) = (x \in (S \cap T), y \in (S \cap T) ⟼ (x H y) \cap (x J y))$
16		infsubc2	$⊢ (H \in Subcat (C) \land J \in Subcat (C)) \to (x \in (dom dom H \cap dom dom J), y \in (dom dom H \cap dom dom J) ⟼ (x H y) \cap (x J y)) \in Subcat (C)$
17	3 4 16	syl2anc	$⊢ φ \to (x \in (dom dom H \cap dom dom J), y \in (dom dom H \cap dom dom J) ⟼ (x H y) \cap (x J y)) \in Subcat (C)$
18	15 17	eqeltrrd	$⊢ φ \to (x \in (S \cap T), y \in (S \cap T) ⟼ (x H y) \cap (x J y)) \in Subcat (C)$

Metamath Proof Explorer