Metamath Proof Explorer

Theorem suppsnop

Description: The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019)

Ref Expression
Hypothesis suppsnop.f 
|- F = { <. X , Y >. }
Assertion suppsnop 
|- ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F supp Z ) = if ( Y = Z , (/) , { X } ) )

Proof

Step Hyp Ref Expression
1 suppsnop.f 
 |-  F = { <. X , Y >. }
2 f1osng 
 |-  ( ( X e. V /\ Y e. W ) -> { <. X , Y >. } : { X } -1-1-onto-> { Y } )
3 f1of 
 |-  ( { <. X , Y >. } : { X } -1-1-onto-> { Y } -> { <. X , Y >. } : { X } --> { Y } )
4 2 3 syl 
 |-  ( ( X e. V /\ Y e. W ) -> { <. X , Y >. } : { X } --> { Y } )
5 4 3adant3 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> { <. X , Y >. } : { X } --> { Y } )
6 1 feq1i 
 |-  ( F : { X } --> { Y } <-> { <. X , Y >. } : { X } --> { Y } )
7 5 6 sylibr 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> F : { X } --> { Y } )
8 snex 
 |-  { X } e. _V
9 fex 
 |-  ( ( F : { X } --> { Y } /\ { X } e. _V ) -> F e. _V )
10 7 8 9 sylancl 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> F e. _V )
11 simp3 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> Z e. U )
12 suppval 
 |-  ( ( F e. _V /\ Z e. U ) -> ( F supp Z ) = { x e. dom F | ( F " { x } ) =/= { Z } } )
13 10 11 12 syl2anc 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F supp Z ) = { x e. dom F | ( F " { x } ) =/= { Z } } )
14 7 fdmd 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> dom F = { X } )
15 14 rabeqdv 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> { x e. dom F | ( F " { x } ) =/= { Z } } = { x e. { X } | ( F " { x } ) =/= { Z } } )
16 sneq 
 |-  ( x = X -> { x } = { X } )
17 16 imaeq2d 
 |-  ( x = X -> ( F " { x } ) = ( F " { X } ) )
18 17 neeq1d 
 |-  ( x = X -> ( ( F " { x } ) =/= { Z } <-> ( F " { X } ) =/= { Z } ) )
19 18 rabsnif 
 |-  { x e. { X } | ( F " { x } ) =/= { Z } } = if ( ( F " { X } ) =/= { Z } , { X } , (/) )
20 15 19 eqtrdi 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> { x e. dom F | ( F " { x } ) =/= { Z } } = if ( ( F " { X } ) =/= { Z } , { X } , (/) ) )
21 7 ffnd 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> F Fn { X } )
22 snidg 
 |-  ( X e. V -> X e. { X } )
23 22 3ad2ant1 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> X e. { X } )
24 fnsnfv 
 |-  ( ( F Fn { X } /\ X e. { X } ) -> { ( F ` X ) } = ( F " { X } ) )
25 24 eqcomd 
 |-  ( ( F Fn { X } /\ X e. { X } ) -> ( F " { X } ) = { ( F ` X ) } )
26 21 23 25 syl2anc 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F " { X } ) = { ( F ` X ) } )
27 26 neeq1d 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( ( F " { X } ) =/= { Z } <-> { ( F ` X ) } =/= { Z } ) )
28 1 fveq1i 
 |-  ( F ` X ) = ( { <. X , Y >. } ` X )
29 fvsng 
 |-  ( ( X e. V /\ Y e. W ) -> ( { <. X , Y >. } ` X ) = Y )
30 29 3adant3 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { <. X , Y >. } ` X ) = Y )
31 28 30 syl5eq 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F ` X ) = Y )
32 31 sneqd 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> { ( F ` X ) } = { Y } )
33 32 neeq1d 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { ( F ` X ) } =/= { Z } <-> { Y } =/= { Z } ) )
34 sneqbg 
 |-  ( Y e. W -> ( { Y } = { Z } <-> Y = Z ) )
35 34 3ad2ant2 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { Y } = { Z } <-> Y = Z ) )
36 35 necon3abid 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( { Y } =/= { Z } <-> -. Y = Z ) )
37 27 33 36 3bitrd 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( ( F " { X } ) =/= { Z } <-> -. Y = Z ) )
38 37 ifbid 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> if ( ( F " { X } ) =/= { Z } , { X } , (/) ) = if ( -. Y = Z , { X } , (/) ) )
39 ifnot 
 |-  if ( -. Y = Z , { X } , (/) ) = if ( Y = Z , (/) , { X } )
40 38 39 eqtrdi 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> if ( ( F " { X } ) =/= { Z } , { X } , (/) ) = if ( Y = Z , (/) , { X } ) )
41 13 20 40 3eqtrd 
 |-  ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F supp Z ) = if ( Y = Z , (/) , { X } ) )