Metamath Proof Explorer

Theorem fpropnf1

Description: A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021)

Ref Expression
Hypothesis fpropnf1.f 
|- F = { <. X , Z >. , <. Y , Z >. }
Assertion fpropnf1 
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Fun F /\ -. Fun `' F ) )

Proof

Step Hyp Ref Expression
1 fpropnf1.f 
 |-  F = { <. X , Z >. , <. Y , Z >. }
2 id 
 |-  ( ( X e. U /\ Y e. V ) -> ( X e. U /\ Y e. V ) )
3 2 3adant3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( X e. U /\ Y e. V ) )
4 3 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( X e. U /\ Y e. V ) )
5 id 
 |-  ( Z e. W -> Z e. W )
6 5 5 jca 
 |-  ( Z e. W -> ( Z e. W /\ Z e. W ) )
7 6 3ad2ant3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( Z e. W /\ Z e. W ) )
8 7 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Z e. W /\ Z e. W ) )
9 simpr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> X =/= Y )
10 4 8 9 3jca 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( X e. U /\ Y e. V ) /\ ( Z e. W /\ Z e. W ) /\ X =/= Y ) )
11 funprg 
 |-  ( ( ( X e. U /\ Y e. V ) /\ ( Z e. W /\ Z e. W ) /\ X =/= Y ) -> Fun { <. X , Z >. , <. Y , Z >. } )
12 10 11 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> Fun { <. X , Z >. , <. Y , Z >. } )
13 1 funeqi 
 |-  ( Fun F <-> Fun { <. X , Z >. , <. Y , Z >. } )
14 12 13 sylibr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> Fun F )
15 neneq 
 |-  ( X =/= Y -> -. X = Y )
16 15 adantl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> -. X = Y )
17 fprg 
 |-  ( ( ( X e. U /\ Y e. V ) /\ ( Z e. W /\ Z e. W ) /\ X =/= Y ) -> { <. X , Z >. , <. Y , Z >. } : { X , Y } --> { Z , Z } )
18 10 17 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> { <. X , Z >. , <. Y , Z >. } : { X , Y } --> { Z , Z } )
19 1 eqcomi 
 |-  { <. X , Z >. , <. Y , Z >. } = F
20 19 feq1i 
 |-  ( { <. X , Z >. , <. Y , Z >. } : { X , Y } --> { Z , Z } <-> F : { X , Y } --> { Z , Z } )
21 18 20 sylib 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> F : { X , Y } --> { Z , Z } )
22 df-f1 
 |-  ( F : { X , Y } -1-1-> { Z , Z } <-> ( F : { X , Y } --> { Z , Z } /\ Fun `' F ) )
23 dff13 
 |-  ( F : { X , Y } -1-1-> { Z , Z } <-> ( F : { X , Y } --> { Z , Z } /\ A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
24 fveqeq2 
 |-  ( x = X -> ( ( F ` x ) = ( F ` y ) <-> ( F ` X ) = ( F ` y ) ) )
25 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
26 24 25 imbi12d 
 |-  ( x = X -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( ( F ` X ) = ( F ` y ) -> X = y ) ) )
27 26 ralbidv 
 |-  ( x = X -> ( A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) ) )
28 fveqeq2 
 |-  ( x = Y -> ( ( F ` x ) = ( F ` y ) <-> ( F ` Y ) = ( F ` y ) ) )
29 eqeq1 
 |-  ( x = Y -> ( x = y <-> Y = y ) )
30 28 29 imbi12d 
 |-  ( x = Y -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) )
31 30 ralbidv 
 |-  ( x = Y -> ( A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) )
32 27 31 ralprg 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) ) )
33 32 3adant3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) ) )
34 33 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) ) )
35 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
36 35 eqeq2d 
 |-  ( y = X -> ( ( F ` X ) = ( F ` y ) <-> ( F ` X ) = ( F ` X ) ) )
37 eqeq2 
 |-  ( y = X -> ( X = y <-> X = X ) )
38 36 37 imbi12d 
 |-  ( y = X -> ( ( ( F ` X ) = ( F ` y ) -> X = y ) <-> ( ( F ` X ) = ( F ` X ) -> X = X ) ) )
39 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
40 39 eqeq2d 
 |-  ( y = Y -> ( ( F ` X ) = ( F ` y ) <-> ( F ` X ) = ( F ` Y ) ) )
41 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
42 40 41 imbi12d 
 |-  ( y = Y -> ( ( ( F ` X ) = ( F ` y ) -> X = y ) <-> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
43 38 42 ralprg 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) <-> ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) )
44 35 eqeq2d 
 |-  ( y = X -> ( ( F ` Y ) = ( F ` y ) <-> ( F ` Y ) = ( F ` X ) ) )
45 eqeq2 
 |-  ( y = X -> ( Y = y <-> Y = X ) )
46 44 45 imbi12d 
 |-  ( y = X -> ( ( ( F ` Y ) = ( F ` y ) -> Y = y ) <-> ( ( F ` Y ) = ( F ` X ) -> Y = X ) ) )
47 39 eqeq2d 
 |-  ( y = Y -> ( ( F ` Y ) = ( F ` y ) <-> ( F ` Y ) = ( F ` Y ) ) )
48 eqeq2 
 |-  ( y = Y -> ( Y = y <-> Y = Y ) )
49 47 48 imbi12d 
 |-  ( y = Y -> ( ( ( F ` Y ) = ( F ` y ) -> Y = y ) <-> ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) )
50 46 49 ralprg 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) <-> ( ( ( F ` Y ) = ( F ` X ) -> Y = X ) /\ ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) ) )
51 43 50 anbi12d 
 |-  ( ( X e. U /\ Y e. V ) -> ( ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) <-> ( ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) /\ ( ( ( F ` Y ) = ( F ` X ) -> Y = X ) /\ ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) ) ) )
52 51 3adant3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) <-> ( ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) /\ ( ( ( F ` Y ) = ( F ` X ) -> Y = X ) /\ ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) ) ) )
53 52 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) <-> ( ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) /\ ( ( ( F ` Y ) = ( F ` X ) -> Y = X ) /\ ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) ) ) )
54 1 fveq1i 
 |-  ( F ` X ) = ( { <. X , Z >. , <. Y , Z >. } ` X )
55 3simpb 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( X e. U /\ Z e. W ) )
56 55 anim1i 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( X e. U /\ Z e. W ) /\ X =/= Y ) )
57 df-3an 
 |-  ( ( X e. U /\ Z e. W /\ X =/= Y ) <-> ( ( X e. U /\ Z e. W ) /\ X =/= Y ) )
58 56 57 sylibr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( X e. U /\ Z e. W /\ X =/= Y ) )
59 fvpr1g 
 |-  ( ( X e. U /\ Z e. W /\ X =/= Y ) -> ( { <. X , Z >. , <. Y , Z >. } ` X ) = Z )
60 58 59 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( { <. X , Z >. , <. Y , Z >. } ` X ) = Z )
61 54 60 syl5eq 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( F ` X ) = Z )
62 1 fveq1i 
 |-  ( F ` Y ) = ( { <. X , Z >. , <. Y , Z >. } ` Y )
63 3simpc 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( Y e. V /\ Z e. W ) )
64 63 anim1i 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( Y e. V /\ Z e. W ) /\ X =/= Y ) )
65 df-3an 
 |-  ( ( Y e. V /\ Z e. W /\ X =/= Y ) <-> ( ( Y e. V /\ Z e. W ) /\ X =/= Y ) )
66 64 65 sylibr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Y e. V /\ Z e. W /\ X =/= Y ) )
67 fvpr2g 
 |-  ( ( Y e. V /\ Z e. W /\ X =/= Y ) -> ( { <. X , Z >. , <. Y , Z >. } ` Y ) = Z )
68 66 67 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( { <. X , Z >. , <. Y , Z >. } ` Y ) = Z )
69 62 68 syl5req 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> Z = ( F ` Y ) )
70 61 69 eqtrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( F ` X ) = ( F ` Y ) )
71 idd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( X = Y -> X = Y ) )
72 70 71 embantd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( ( F ` X ) = ( F ` Y ) -> X = Y ) -> X = Y ) )
73 72 adantld 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) -> X = Y ) )
74 73 adantrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( ( ( ( F ` X ) = ( F ` X ) -> X = X ) /\ ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) /\ ( ( ( F ` Y ) = ( F ` X ) -> Y = X ) /\ ( ( F ` Y ) = ( F ` Y ) -> Y = Y ) ) ) -> X = Y ) )
75 53 74 sylbid 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( A. y e. { X , Y } ( ( F ` X ) = ( F ` y ) -> X = y ) /\ A. y e. { X , Y } ( ( F ` Y ) = ( F ` y ) -> Y = y ) ) -> X = Y ) )
76 34 75 sylbid 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) -> X = Y ) )
77 76 adantld 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( F : { X , Y } --> { Z , Z } /\ A. x e. { X , Y } A. y e. { X , Y } ( ( F ` x ) = ( F ` y ) -> x = y ) ) -> X = Y ) )
78 23 77 syl5bi 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( F : { X , Y } -1-1-> { Z , Z } -> X = Y ) )
79 22 78 syl5bir 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( ( F : { X , Y } --> { Z , Z } /\ Fun `' F ) -> X = Y ) )
80 21 79 mpand 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Fun `' F -> X = Y ) )
81 16 80 mtod 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> -. Fun `' F )
82 14 81 jca 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Fun F /\ -. Fun `' F ) )