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

Metamath Proof Explorer

Theorem f12dfv

Description: A one-to-one function with a domain with at least two different elements in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018)

Ref Expression
Hypothesis f12dfv.a 
|- A = { X , Y }
Assertion f12dfv 
|- ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( F : A -1-1-> B <-> ( F : A --> B /\ ( F ` X ) =/= ( F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 f12dfv.a 
 |-  A = { X , Y }
2 dff14b 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )
3 1 raleqi 
 |-  ( A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. x e. { X , Y } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
4 sneq 
 |-  ( x = X -> { x } = { X } )
5 4 difeq2d 
 |-  ( x = X -> ( A \ { x } ) = ( A \ { X } ) )
6 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
7 6 neeq1d 
 |-  ( x = X -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` y ) ) )
8 5 7 raleqbidv 
 |-  ( x = X -> ( A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) ) )
9 sneq 
 |-  ( x = Y -> { x } = { Y } )
10 9 difeq2d 
 |-  ( x = Y -> ( A \ { x } ) = ( A \ { Y } ) )
11 fveq2 
 |-  ( x = Y -> ( F ` x ) = ( F ` Y ) )
12 11 neeq1d 
 |-  ( x = Y -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` y ) ) )
13 10 12 raleqbidv 
 |-  ( x = Y -> ( A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) )
14 8 13 ralprg 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. x e. { X , Y } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) ) )
15 14 adantr 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. x e. { X , Y } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) ) )
16 1 difeq1i 
 |-  ( A \ { X } ) = ( { X , Y } \ { X } )
17 difprsn1 
 |-  ( X =/= Y -> ( { X , Y } \ { X } ) = { Y } )
18 16 17 eqtrid 
 |-  ( X =/= Y -> ( A \ { X } ) = { Y } )
19 18 adantl 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A \ { X } ) = { Y } )
20 19 raleqdv 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) <-> A. y e. { Y } ( F ` X ) =/= ( F ` y ) ) )
21 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
22 21 neeq2d 
 |-  ( y = Y -> ( ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
23 22 ralsng 
 |-  ( Y e. V -> ( A. y e. { Y } ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
24 23 adantl 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. y e. { Y } ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
25 24 adantr 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. { Y } ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
26 20 25 bitrd 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
27 1 difeq1i 
 |-  ( A \ { Y } ) = ( { X , Y } \ { Y } )
28 difprsn2 
 |-  ( X =/= Y -> ( { X , Y } \ { Y } ) = { X } )
29 27 28 eqtrid 
 |-  ( X =/= Y -> ( A \ { Y } ) = { X } )
30 29 adantl 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A \ { Y } ) = { X } )
31 30 raleqdv 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) <-> A. y e. { X } ( F ` Y ) =/= ( F ` y ) ) )
32 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
33 32 neeq2d 
 |-  ( y = X -> ( ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
34 33 ralsng 
 |-  ( X e. U -> ( A. y e. { X } ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
35 34 adantr 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. y e. { X } ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
36 35 adantr 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. { X } ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
37 31 36 bitrd 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
38 26 37 anbi12d 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` X ) ) ) )
39 necom 
 |-  ( ( F ` X ) =/= ( F ` Y ) <-> ( F ` Y ) =/= ( F ` X ) )
40 39 biimpi 
 |-  ( ( F ` X ) =/= ( F ` Y ) -> ( F ` Y ) =/= ( F ` X ) )
41 40 pm4.71i 
 |-  ( ( F ` X ) =/= ( F ` Y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` X ) ) )
42 38 41 bitr4di 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) <-> ( F ` X ) =/= ( F ` Y ) ) )
43 15 42 bitrd 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. x e. { X , Y } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
44 3 43 bitrid 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
45 44 anbi2d 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) <-> ( F : A --> B /\ ( F ` X ) =/= ( F ` Y ) ) ) )
46 2 45 bitrid 
 |-  ( ( ( X e. U /\ Y e. V ) /\ X =/= Y ) -> ( F : A -1-1-> B <-> ( F : A --> B /\ ( F ` X ) =/= ( F ` Y ) ) ) )