Theorem infsubc2d

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

	Ref	Expression
Hypotheses	infsubc2d.1	|- ( ph -> H Fn ( S X. S ) )
	infsubc2d.2	|- ( ph -> J Fn ( T X. T ) )
	infsubc2d.3	|- ( ph -> H e. ( Subcat ` C ) )
	infsubc2d.4	|- ( ph -> J e. ( Subcat ` C ) )
Assertion	infsubc2d	|- ( ph -> ( x e. ( S i^i T ) , y e. ( S i^i T ) |-> ( ( x H y ) i^i ( x J y ) ) ) e. ( Subcat ` C ) )

Proof

Step	Hyp	Ref	Expression
1		infsubc2d.1	|- ( ph -> H Fn ( S X. S ) )
2		infsubc2d.2	|- ( ph -> J Fn ( T X. T ) )
3		infsubc2d.3	|- ( ph -> H e. ( Subcat ` C ) )
4		infsubc2d.4	|- ( ph -> J e. ( Subcat ` C ) )
5	1	fndmd	|- ( ph -> dom H = ( S X. S ) )
6	5	dmeqd	|- ( ph -> dom dom H = dom ( S X. S ) )
7		dmxpid	|- dom ( S X. S ) = S
8	6 7	eqtrdi	|- ( ph -> dom dom H = S )
9	2	fndmd	|- ( ph -> dom J = ( T X. T ) )
10	9	dmeqd	|- ( ph -> dom dom J = dom ( T X. T ) )
11		dmxpid	|- dom ( T X. T ) = T
12	10 11	eqtrdi	|- ( ph -> dom dom J = T )
13	8 12	ineq12d	|- ( ph -> ( dom dom H i^i dom dom J ) = ( S i^i T ) )
14		mpoeq12	|- ( ( ( dom dom H i^i dom dom J ) = ( S i^i T ) /\ ( dom dom H i^i dom dom J ) = ( S i^i T ) ) -> ( x e. ( dom dom H i^i dom dom J ) , y e. ( dom dom H i^i dom dom J ) |-> ( ( x H y ) i^i ( x J y ) ) ) = ( x e. ( S i^i T ) , y e. ( S i^i T ) |-> ( ( x H y ) i^i ( x J y ) ) ) )
15	13 13 14	syl2anc	|- ( ph -> ( x e. ( dom dom H i^i dom dom J ) , y e. ( dom dom H i^i dom dom J ) |-> ( ( x H y ) i^i ( x J y ) ) ) = ( x e. ( S i^i T ) , y e. ( S i^i T ) |-> ( ( x H y ) i^i ( x J y ) ) ) )
16		infsubc2	|- ( ( H e. ( Subcat ` C ) /\ J e. ( Subcat ` C ) ) -> ( x e. ( dom dom H i^i dom dom J ) , y e. ( dom dom H i^i dom dom J ) |-> ( ( x H y ) i^i ( x J y ) ) ) e. ( Subcat ` C ) )
17	3 4 16	syl2anc	|- ( ph -> ( x e. ( dom dom H i^i dom dom J ) , y e. ( dom dom H i^i dom dom J ) |-> ( ( x H y ) i^i ( x J y ) ) ) e. ( Subcat ` C ) )
18	15 17	eqeltrrd	|- ( ph -> ( x e. ( S i^i T ) , y e. ( S i^i T ) |-> ( ( x H y ) i^i ( x J y ) ) ) e. ( Subcat ` C ) )