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 e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 prnzg 
 |-  ( A e. ( Subcat ` C ) -> { A , B } =/= (/) )
2 1 adantr 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> { A , B } =/= (/) )
3 simpll 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> A e. ( Subcat ` C ) )
4 eleq1 
 |-  ( y = A -> ( y e. ( Subcat ` C ) <-> A e. ( Subcat ` C ) ) )
5 3 4 syl5ibrcom 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> ( y = A -> y e. ( Subcat ` C ) ) )
6 simplr 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> B e. ( Subcat ` C ) )
7 eleq1 
 |-  ( y = B -> ( y e. ( Subcat ` C ) <-> B e. ( Subcat ` C ) ) )
8 6 7 syl5ibrcom 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> ( y = B -> y e. ( Subcat ` C ) ) )
9 elpri 
 |-  ( y e. { A , B } -> ( y = A \/ y = B ) )
10 9 adantl 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> ( y = A \/ y = B ) )
11 5 8 10 mpjaod 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ y e. { A , B } ) -> y e. ( Subcat ` C ) )
12 iinfprg 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) = ( x e. |^|_ y e. { A , B } dom y |-> |^|_ y e. { A , B } ( y ` x ) ) )
13 2 11 12 iinfsubc 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. ( dom A i^i dom B ) |-> ( ( A ` x ) i^i ( B ` x ) ) ) e. ( Subcat ` C ) )