Theorem infsubc2

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

	Ref	Expression
Assertion	infsubc2	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) , 𝑦 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) ↦ ( ( 𝑥 𝐴 𝑦 ) ∩ ( 𝑥 𝐵 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prnzg	⊢ ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) → { 𝐴 , 𝐵 } ≠ ∅ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → { 𝐴 , 𝐵 } ≠ ∅ )
3		simpll	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → 𝐴 ∈ ( Subcat ‘ 𝐶 ) )
4		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5	3 4	subcssc	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → 𝐴 ⊆cat ( Homf ‘ 𝐶 ) )
6		breq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 ⊆cat ( Homf ‘ 𝐶 ) ↔ 𝐴 ⊆cat ( Homf ‘ 𝐶 ) ) )
7	5 6	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → ( 𝑤 = 𝐴 → 𝑤 ⊆cat ( Homf ‘ 𝐶 ) ) )
8		simplr	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → 𝐵 ∈ ( Subcat ‘ 𝐶 ) )
9	8 4	subcssc	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → 𝐵 ⊆cat ( Homf ‘ 𝐶 ) )
10		breq1	⊢ ( 𝑤 = 𝐵 → ( 𝑤 ⊆cat ( Homf ‘ 𝐶 ) ↔ 𝐵 ⊆cat ( Homf ‘ 𝐶 ) ) )
11	9 10	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → ( 𝑤 = 𝐵 → 𝑤 ⊆cat ( Homf ‘ 𝐶 ) ) )
12		elpri	⊢ ( 𝑤 ∈ { 𝐴 , 𝐵 } → ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
14	7 11 13	mpjaod	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → 𝑤 ⊆cat ( Homf ‘ 𝐶 ) )
15		iinfprg	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑧 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ∩ ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom 𝑤 ↦ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝑤 ‘ 𝑧 ) ) )
16		eqidd	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑤 ∈ { 𝐴 , 𝐵 } ) → dom dom 𝑤 = dom dom 𝑤 )
17		nfv	⊢ Ⅎ 𝑤 ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) )
18	2 14 15 16 17	iinfssclem1	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑧 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ∩ ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom dom 𝑤 , 𝑦 ∈ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom dom 𝑤 ↦ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝑥 𝑤 𝑦 ) ) )
19		dmeq	⊢ ( 𝑤 = 𝐴 → dom 𝑤 = dom 𝐴 )
20	19	dmeqd	⊢ ( 𝑤 = 𝐴 → dom dom 𝑤 = dom dom 𝐴 )
21		dmeq	⊢ ( 𝑤 = 𝐵 → dom 𝑤 = dom 𝐵 )
22	21	dmeqd	⊢ ( 𝑤 = 𝐵 → dom dom 𝑤 = dom dom 𝐵 )
23	20 22	iinxprg	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom dom 𝑤 = ( dom dom 𝐴 ∩ dom dom 𝐵 ) )
24		oveq	⊢ ( 𝑤 = 𝐴 → ( 𝑥 𝑤 𝑦 ) = ( 𝑥 𝐴 𝑦 ) )
25		oveq	⊢ ( 𝑤 = 𝐵 → ( 𝑥 𝑤 𝑦 ) = ( 𝑥 𝐵 𝑦 ) )
26	24 25	iinxprg	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ∩ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝑥 𝑤 𝑦 ) = ( ( 𝑥 𝐴 𝑦 ) ∩ ( 𝑥 𝐵 𝑦 ) ) )
27	23 23 26	mpoeq123dv	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom dom 𝑤 , 𝑦 ∈ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } dom dom 𝑤 ↦ ∩ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝑥 𝑤 𝑦 ) ) = ( 𝑥 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) , 𝑦 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) ↦ ( ( 𝑥 𝐴 𝑦 ) ∩ ( 𝑥 𝐵 𝑦 ) ) ) )
28	18 27	eqtrd	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑧 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ∩ ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) , 𝑦 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) ↦ ( ( 𝑥 𝐴 𝑦 ) ∩ ( 𝑥 𝐵 𝑦 ) ) ) )
29		infsubc	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑧 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ∩ ( 𝐵 ‘ 𝑧 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )
30	28 29	eqeltrrd	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) , 𝑦 ∈ ( dom dom 𝐴 ∩ dom dom 𝐵 ) ↦ ( ( 𝑥 𝐴 𝑦 ) ∩ ( 𝑥 𝐵 𝑦 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )