Metamath Proof Explorer

Theorem infsubc

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

Ref Expression
Assertion infsubc ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C → x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x ∈ Subcat ⁡ C

Proof

Step Hyp Ref Expression
1 prnzg ⊢ A ∈ Subcat ⁡ C → A B ≠ ∅
2 1 adantr ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C → A B ≠ ∅
3 simpll ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → A ∈ Subcat ⁡ C
4 eleq1 ⊢ y = A → y ∈ Subcat ⁡ C ↔ A ∈ Subcat ⁡ C
5 3 4 syl5ibrcom ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → y = A → y ∈ Subcat ⁡ C
6 simplr ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → B ∈ Subcat ⁡ C
7 eleq1 ⊢ y = B → y ∈ Subcat ⁡ C ↔ B ∈ Subcat ⁡ C
8 6 7 syl5ibrcom ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → y = B → y ∈ Subcat ⁡ C
9 elpri ⊢ y ∈ A B → y = A ∨ y = B
10 9 adantl ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → y = A ∨ y = B
11 5 8 10 mpjaod ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C ∧ y ∈ A B → y ∈ Subcat ⁡ C
12 iinfprg ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C → x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x = x ∈ ⋂ y ∈ A B dom ⁡ y ⟼ ⋂ y ∈ A B y ⁡ x
13 2 11 12 iinfsubc ⊢ A ∈ Subcat ⁡ C ∧ B ∈ Subcat ⁡ C → x ∈ dom ⁡ A ∩ dom ⁡ B ⟼ A ⁡ x ∩ B ⁡ x ∈ Subcat ⁡ C