Theorem infsubc2d

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

	Ref	Expression
Hypotheses	infsubc2d.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	infsubc2d.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
	infsubc2d.3	⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
	infsubc2d.4	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
Assertion	infsubc2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) , 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		infsubc2d.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
2		infsubc2d.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
3		infsubc2d.3	⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
4		infsubc2d.4	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
5	1	fndmd	⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
6	5	dmeqd	⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
7		dmxpid	⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
8	6 7	eqtrdi	⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
9	2	fndmd	⊢ ( 𝜑 → dom 𝐽 = ( 𝑇 × 𝑇 ) )
10	9	dmeqd	⊢ ( 𝜑 → dom dom 𝐽 = dom ( 𝑇 × 𝑇 ) )
11		dmxpid	⊢ dom ( 𝑇 × 𝑇 ) = 𝑇
12	10 11	eqtrdi	⊢ ( 𝜑 → dom dom 𝐽 = 𝑇 )
13	8 12	ineq12d	⊢ ( 𝜑 → ( dom dom 𝐻 ∩ dom dom 𝐽 ) = ( 𝑆 ∩ 𝑇 ) )
14		mpoeq12	⊢ ( ( ( dom dom 𝐻 ∩ dom dom 𝐽 ) = ( 𝑆 ∩ 𝑇 ) ∧ ( dom dom 𝐻 ∩ dom dom 𝐽 ) = ( 𝑆 ∩ 𝑇 ) ) → ( 𝑥 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) , 𝑦 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) , 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) )
15	13 13 14	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) , 𝑦 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) , 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) )
16		infsubc2	⊢ ( ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) , 𝑦 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )
17	3 4 16	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) , 𝑦 ∈ ( dom dom 𝐻 ∩ dom dom 𝐽 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )
18	15 17	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) , 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ↦ ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑥 𝐽 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )