Metamath Proof Explorer

Theorem arwhoma

Description: An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwrcl.a 
|- A = ( Arrow ` C )
arwhoma.h 
|- H = ( HomA ` C )
Assertion arwhoma 
|- ( F e. A -> F e. ( ( domA ` F ) H ( codA ` F ) ) )

Proof

Step Hyp Ref Expression
1 arwrcl.a 
 |-  A = ( Arrow ` C )
2 arwhoma.h 
 |-  H = ( HomA ` C )
3 1 2 arwval 
 |-  A = U. ran H
4 3 eleq2i 
 |-  ( F e. A <-> F e. U. ran H )
5 4 biimpi 
 |-  ( F e. A -> F e. U. ran H )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 1 arwrcl 
 |-  ( F e. A -> C e. Cat )
8 2 6 7 homaf 
 |-  ( F e. A -> H : ( ( Base ` C ) X. ( Base ` C ) ) --> ~P ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) )
9 ffn 
 |-  ( H : ( ( Base ` C ) X. ( Base ` C ) ) --> ~P ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) )
10 fnunirn 
 |-  ( H Fn ( ( Base ` C ) X. ( Base ` C ) ) -> ( F e. U. ran H <-> E. z e. ( ( Base ` C ) X. ( Base ` C ) ) F e. ( H ` z ) ) )
11 8 9 10 3syl 
 |-  ( F e. A -> ( F e. U. ran H <-> E. z e. ( ( Base ` C ) X. ( Base ` C ) ) F e. ( H ` z ) ) )
12 5 11 mpbid 
 |-  ( F e. A -> E. z e. ( ( Base ` C ) X. ( Base ` C ) ) F e. ( H ` z ) )
13 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
14 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
15 13 14 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
16 15 eleq2d 
 |-  ( z = <. x , y >. -> ( F e. ( H ` z ) <-> F e. ( x H y ) ) )
17 16 rexxp 
 |-  ( E. z e. ( ( Base ` C ) X. ( Base ` C ) ) F e. ( H ` z ) <-> E. x e. ( Base ` C ) E. y e. ( Base ` C ) F e. ( x H y ) )
18 12 17 sylib 
 |-  ( F e. A -> E. x e. ( Base ` C ) E. y e. ( Base ` C ) F e. ( x H y ) )
19 id 
 |-  ( F e. ( x H y ) -> F e. ( x H y ) )
20 2 homadm 
 |-  ( F e. ( x H y ) -> ( domA ` F ) = x )
21 2 homacd 
 |-  ( F e. ( x H y ) -> ( codA ` F ) = y )
22 20 21 oveq12d 
 |-  ( F e. ( x H y ) -> ( ( domA ` F ) H ( codA ` F ) ) = ( x H y ) )
23 19 22 eleqtrrd 
 |-  ( F e. ( x H y ) -> F e. ( ( domA ` F ) H ( codA ` F ) ) )
24 23 rexlimivw 
 |-  ( E. y e. ( Base ` C ) F e. ( x H y ) -> F e. ( ( domA ` F ) H ( codA ` F ) ) )
25 24 rexlimivw 
 |-  ( E. x e. ( Base ` C ) E. y e. ( Base ` C ) F e. ( x H y ) -> F e. ( ( domA ` F ) H ( codA ` F ) ) )
26 18 25 syl 
 |-  ( F e. A -> F e. ( ( domA ` F ) H ( codA ` F ) ) )