Theorem infsubc

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

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

Proof

Step	Hyp	Ref	Expression
1		prnzg	⊢ ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) → { 𝐴 , 𝐵 } ≠ ∅ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → { 𝐴 , 𝐵 } ≠ ∅ )
3		simpll	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → 𝐴 ∈ ( Subcat ‘ 𝐶 ) )
4		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( Subcat ‘ 𝐶 ) ↔ 𝐴 ∈ ( Subcat ‘ 𝐶 ) ) )
5	3 4	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → ( 𝑦 = 𝐴 → 𝑦 ∈ ( Subcat ‘ 𝐶 ) ) )
6		simplr	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → 𝐵 ∈ ( Subcat ‘ 𝐶 ) )
7		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ ( Subcat ‘ 𝐶 ) ↔ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) )
8	6 7	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → ( 𝑦 = 𝐵 → 𝑦 ∈ ( Subcat ‘ 𝐶 ) ) )
9		elpri	⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } → ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
10	9	adantl	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
11	5 8 10	mpjaod	⊢ ( ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) → 𝑦 ∈ ( Subcat ‘ 𝐶 ) )
12		iinfprg	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } dom 𝑦 ↦ ∩ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ‘ 𝑥 ) ) )
13	2 11 12	iinfsubc	⊢ ( ( 𝐴 ∈ ( Subcat ‘ 𝐶 ) ∧ 𝐵 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝑥 ∈ ( dom 𝐴 ∩ dom 𝐵 ) ↦ ( ( 𝐴 ‘ 𝑥 ) ∩ ( 𝐵 ‘ 𝑥 ) ) ) ∈ ( Subcat ‘ 𝐶 ) )