This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem homaf

Description: Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homarcl.h 
|- H = ( HomA ` C )
homafval.b 
|- B = ( Base ` C )
homafval.c 
|- ( ph -> C e. Cat )
Assertion homaf 
|- ( ph -> H : ( B X. B ) --> ~P ( ( B X. B ) X. _V ) )

Proof

Step Hyp Ref Expression
1 homarcl.h 
 |-  H = ( HomA ` C )
2 homafval.b 
 |-  B = ( Base ` C )
3 homafval.c 
 |-  ( ph -> C e. Cat )
4 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 1 2 3 4 homafval 
 |-  ( ph -> H = ( x e. ( B X. B ) |-> ( { x } X. ( ( Hom ` C ) ` x ) ) ) )
6 snssi 
 |-  ( x e. ( B X. B ) -> { x } C_ ( B X. B ) )
7 6 adantl 
 |-  ( ( ph /\ x e. ( B X. B ) ) -> { x } C_ ( B X. B ) )
8 ssv 
 |-  ( ( Hom ` C ) ` x ) C_ _V
9 xpss12 
 |-  ( ( { x } C_ ( B X. B ) /\ ( ( Hom ` C ) ` x ) C_ _V ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
10 7 8 9 sylancl 
 |-  ( ( ph /\ x e. ( B X. B ) ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
11 vsnex 
 |-  { x } e. _V
12 fvex 
 |-  ( ( Hom ` C ) ` x ) e. _V
13 11 12 xpex 
 |-  ( { x } X. ( ( Hom ` C ) ` x ) ) e. _V
14 13 elpw 
 |-  ( ( { x } X. ( ( Hom ` C ) ` x ) ) e. ~P ( ( B X. B ) X. _V ) <-> ( { x } X. ( ( Hom ` C ) ` x ) ) C_ ( ( B X. B ) X. _V ) )
15 10 14 sylibr 
 |-  ( ( ph /\ x e. ( B X. B ) ) -> ( { x } X. ( ( Hom ` C ) ` x ) ) e. ~P ( ( B X. B ) X. _V ) )
16 5 15 fmpt3d 
 |-  ( ph -> H : ( B X. B ) --> ~P ( ( B X. B ) X. _V ) )