Metamath Proof Explorer

Theorem infsubc2

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

Ref Expression
Assertion infsubc2 
|- ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. ( dom dom A i^i dom dom B ) , y e. ( dom dom A i^i dom dom B ) |-> ( ( x A y ) i^i ( x B y ) ) ) 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 ) ) /\ w e. { A , B } ) -> A e. ( Subcat ` C ) )
4 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
5 3 4 subcssc 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> A C_cat ( Homf ` C ) )
6 breq1 
 |-  ( w = A -> ( w C_cat ( Homf ` C ) <-> A C_cat ( Homf ` C ) ) )
7 5 6 syl5ibrcom 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> ( w = A -> w C_cat ( Homf ` C ) ) )
8 simplr 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> B e. ( Subcat ` C ) )
9 8 4 subcssc 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> B C_cat ( Homf ` C ) )
10 breq1 
 |-  ( w = B -> ( w C_cat ( Homf ` C ) <-> B C_cat ( Homf ` C ) ) )
11 9 10 syl5ibrcom 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> ( w = B -> w C_cat ( Homf ` C ) ) )
12 elpri 
 |-  ( w e. { A , B } -> ( w = A \/ w = B ) )
13 12 adantl 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> ( w = A \/ w = B ) )
14 7 11 13 mpjaod 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> w C_cat ( Homf ` C ) )
15 iinfprg 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( z e. ( dom A i^i dom B ) |-> ( ( A ` z ) i^i ( B ` z ) ) ) = ( z e. |^|_ w e. { A , B } dom w |-> |^|_ w e. { A , B } ( w ` z ) ) )
16 eqidd 
 |-  ( ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) /\ w e. { A , B } ) -> dom dom w = dom dom w )
17 nfv 
 |-  F/ w ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) )
18 2 14 15 16 17 iinfssclem1 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( z e. ( dom A i^i dom B ) |-> ( ( A ` z ) i^i ( B ` z ) ) ) = ( x e. |^|_ w e. { A , B } dom dom w , y e. |^|_ w e. { A , B } dom dom w |-> |^|_ w e. { A , B } ( x w y ) ) )
19 dmeq 
 |-  ( w = A -> dom w = dom A )
20 19 dmeqd 
 |-  ( w = A -> dom dom w = dom dom A )
21 dmeq 
 |-  ( w = B -> dom w = dom B )
22 21 dmeqd 
 |-  ( w = B -> dom dom w = dom dom B )
23 20 22 iinxprg 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> |^|_ w e. { A , B } dom dom w = ( dom dom A i^i dom dom B ) )
24 oveq 
 |-  ( w = A -> ( x w y ) = ( x A y ) )
25 oveq 
 |-  ( w = B -> ( x w y ) = ( x B y ) )
26 24 25 iinxprg 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> |^|_ w e. { A , B } ( x w y ) = ( ( x A y ) i^i ( x B y ) ) )
27 23 23 26 mpoeq123dv 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. |^|_ w e. { A , B } dom dom w , y e. |^|_ w e. { A , B } dom dom w |-> |^|_ w e. { A , B } ( x w y ) ) = ( x e. ( dom dom A i^i dom dom B ) , y e. ( dom dom A i^i dom dom B ) |-> ( ( x A y ) i^i ( x B y ) ) ) )
28 18 27 eqtrd 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( z e. ( dom A i^i dom B ) |-> ( ( A ` z ) i^i ( B ` z ) ) ) = ( x e. ( dom dom A i^i dom dom B ) , y e. ( dom dom A i^i dom dom B ) |-> ( ( x A y ) i^i ( x B y ) ) ) )
29 infsubc 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( z e. ( dom A i^i dom B ) |-> ( ( A ` z ) i^i ( B ` z ) ) ) e. ( Subcat ` C ) )
30 28 29 eqeltrrd 
 |-  ( ( A e. ( Subcat ` C ) /\ B e. ( Subcat ` C ) ) -> ( x e. ( dom dom A i^i dom dom B ) , y e. ( dom dom A i^i dom dom B ) |-> ( ( x A y ) i^i ( x B y ) ) ) e. ( Subcat ` C ) )