Metamath Proof Explorer

Theorem f1prex

Description: Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Hypotheses f1prex.1 
|- ( x = ( f ` A ) -> ( ps <-> ch ) )
f1prex.2 
|- ( y = ( f ` B ) -> ( ch <-> ph ) )
Assertion f1prex 
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> ( E. f ( f : { A , B } -1-1-> D /\ ph ) <-> E. x e. D E. y e. D ( x =/= y /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 f1prex.1 
 |-  ( x = ( f ` A ) -> ( ps <-> ch ) )
2 f1prex.2 
 |-  ( y = ( f ` B ) -> ( ch <-> ph ) )
3 simpl1 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> A e. V )
4 simpl2 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> B e. W )
5 simprl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> f : { A , B } -1-1-> D )
6 f1f 
 |-  ( f : { A , B } -1-1-> D -> f : { A , B } --> D )
7 5 6 syl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> f : { A , B } --> D )
8 fpr2g 
 |-  ( ( A e. V /\ B e. W ) -> ( f : { A , B } --> D <-> ( ( f ` A ) e. D /\ ( f ` B ) e. D /\ f = { <. A , ( f ` A ) >. , <. B , ( f ` B ) >. } ) ) )
9 8 biimpa 
 |-  ( ( ( A e. V /\ B e. W ) /\ f : { A , B } --> D ) -> ( ( f ` A ) e. D /\ ( f ` B ) e. D /\ f = { <. A , ( f ` A ) >. , <. B , ( f ` B ) >. } ) )
10 9 simp1d 
 |-  ( ( ( A e. V /\ B e. W ) /\ f : { A , B } --> D ) -> ( f ` A ) e. D )
11 3 4 7 10 syl21anc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ( f ` A ) e. D )
12 9 simp2d 
 |-  ( ( ( A e. V /\ B e. W ) /\ f : { A , B } --> D ) -> ( f ` B ) e. D )
13 3 4 7 12 syl21anc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ( f ` B ) e. D )
14 prid1g 
 |-  ( A e. V -> A e. { A , B } )
15 3 14 syl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> A e. { A , B } )
16 prid2g 
 |-  ( B e. W -> B e. { A , B } )
17 4 16 syl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> B e. { A , B } )
18 15 17 jca 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ( A e. { A , B } /\ B e. { A , B } ) )
19 simpl3 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> A =/= B )
20 f1veqaeq 
 |-  ( ( f : { A , B } -1-1-> D /\ ( A e. { A , B } /\ B e. { A , B } ) ) -> ( ( f ` A ) = ( f ` B ) -> A = B ) )
21 20 necon3d 
 |-  ( ( f : { A , B } -1-1-> D /\ ( A e. { A , B } /\ B e. { A , B } ) ) -> ( A =/= B -> ( f ` A ) =/= ( f ` B ) ) )
22 21 imp 
 |-  ( ( ( f : { A , B } -1-1-> D /\ ( A e. { A , B } /\ B e. { A , B } ) ) /\ A =/= B ) -> ( f ` A ) =/= ( f ` B ) )
23 5 18 19 22 syl21anc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ( f ` A ) =/= ( f ` B ) )
24 simprr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ph )
25 23 24 jca 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> ( ( f ` A ) =/= ( f ` B ) /\ ph ) )
26 neeq1 
 |-  ( x = ( f ` A ) -> ( x =/= y <-> ( f ` A ) =/= y ) )
27 26 1 anbi12d 
 |-  ( x = ( f ` A ) -> ( ( x =/= y /\ ps ) <-> ( ( f ` A ) =/= y /\ ch ) ) )
28 neeq2 
 |-  ( y = ( f ` B ) -> ( ( f ` A ) =/= y <-> ( f ` A ) =/= ( f ` B ) ) )
29 28 2 anbi12d 
 |-  ( y = ( f ` B ) -> ( ( ( f ` A ) =/= y /\ ch ) <-> ( ( f ` A ) =/= ( f ` B ) /\ ph ) ) )
30 27 29 rspc2ev 
 |-  ( ( ( f ` A ) e. D /\ ( f ` B ) e. D /\ ( ( f ` A ) =/= ( f ` B ) /\ ph ) ) -> E. x e. D E. y e. D ( x =/= y /\ ps ) )
31 11 13 25 30 syl3anc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( f : { A , B } -1-1-> D /\ ph ) ) -> E. x e. D E. y e. D ( x =/= y /\ ps ) )
32 31 ex 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( f : { A , B } -1-1-> D /\ ph ) -> E. x e. D E. y e. D ( x =/= y /\ ps ) ) )
33 32 exlimdv 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( E. f ( f : { A , B } -1-1-> D /\ ph ) -> E. x e. D E. y e. D ( x =/= y /\ ps ) ) )
34 simpll1 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> A e. V )
35 simplrl 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> x e. D )
36 34 35 jca 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> ( A e. V /\ x e. D ) )
37 simpll2 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> B e. W )
38 simplrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> y e. D )
39 37 38 jca 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> ( B e. W /\ y e. D ) )
40 simpll3 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> A =/= B )
41 simprl 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> x =/= y )
42 f1oprg 
 |-  ( ( ( A e. V /\ x e. D ) /\ ( B e. W /\ y e. D ) ) -> ( ( A =/= B /\ x =/= y ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-onto-> { x , y } ) )
43 42 imp 
 |-  ( ( ( ( A e. V /\ x e. D ) /\ ( B e. W /\ y e. D ) ) /\ ( A =/= B /\ x =/= y ) ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-onto-> { x , y } )
44 36 39 40 41 43 syl22anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-onto-> { x , y } )
45 f1of1 
 |-  ( { <. A , x >. , <. B , y >. } : { A , B } -1-1-onto-> { x , y } -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-> { x , y } )
46 44 45 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-> { x , y } )
47 35 38 prssd 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> { x , y } C_ D )
48 f1ss 
 |-  ( ( { <. A , x >. , <. B , y >. } : { A , B } -1-1-> { x , y } /\ { x , y } C_ D ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-> D )
49 46 47 48 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> { <. A , x >. , <. B , y >. } : { A , B } -1-1-> D )
50 fvpr1g 
 |-  ( ( A e. V /\ x e. D /\ A =/= B ) -> ( { <. A , x >. , <. B , y >. } ` A ) = x )
51 50 eqcomd 
 |-  ( ( A e. V /\ x e. D /\ A =/= B ) -> x = ( { <. A , x >. , <. B , y >. } ` A ) )
52 34 35 40 51 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> x = ( { <. A , x >. , <. B , y >. } ` A ) )
53 fvpr2g 
 |-  ( ( B e. W /\ y e. D /\ A =/= B ) -> ( { <. A , x >. , <. B , y >. } ` B ) = y )
54 53 eqcomd 
 |-  ( ( B e. W /\ y e. D /\ A =/= B ) -> y = ( { <. A , x >. , <. B , y >. } ` B ) )
55 37 38 40 54 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> y = ( { <. A , x >. , <. B , y >. } ` B ) )
56 prex 
 |-  { <. A , x >. , <. B , y >. } e. _V
57 f1eq1 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( f : { A , B } -1-1-> D <-> { <. A , x >. , <. B , y >. } : { A , B } -1-1-> D ) )
58 fveq1 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( f ` A ) = ( { <. A , x >. , <. B , y >. } ` A ) )
59 58 eqeq2d 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( x = ( f ` A ) <-> x = ( { <. A , x >. , <. B , y >. } ` A ) ) )
60 fveq1 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( f ` B ) = ( { <. A , x >. , <. B , y >. } ` B ) )
61 60 eqeq2d 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( y = ( f ` B ) <-> y = ( { <. A , x >. , <. B , y >. } ` B ) ) )
62 59 61 anbi12d 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( ( x = ( f ` A ) /\ y = ( f ` B ) ) <-> ( x = ( { <. A , x >. , <. B , y >. } ` A ) /\ y = ( { <. A , x >. , <. B , y >. } ` B ) ) ) )
63 57 62 anbi12d 
 |-  ( f = { <. A , x >. , <. B , y >. } -> ( ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) <-> ( { <. A , x >. , <. B , y >. } : { A , B } -1-1-> D /\ ( x = ( { <. A , x >. , <. B , y >. } ` A ) /\ y = ( { <. A , x >. , <. B , y >. } ` B ) ) ) ) )
64 56 63 spcev 
 |-  ( ( { <. A , x >. , <. B , y >. } : { A , B } -1-1-> D /\ ( x = ( { <. A , x >. , <. B , y >. } ` A ) /\ y = ( { <. A , x >. , <. B , y >. } ` B ) ) ) -> E. f ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) )
65 49 52 55 64 syl12anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> E. f ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) )
66 simprl 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> f : { A , B } -1-1-> D )
67 simplrr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ps )
68 simprrl 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> x = ( f ` A ) )
69 68 1 syl 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ( ps <-> ch ) )
70 67 69 mpbid 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ch )
71 simprrr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> y = ( f ` B ) )
72 71 2 syl 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ( ch <-> ph ) )
73 70 72 mpbid 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ph )
74 66 73 jca 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) /\ ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) ) -> ( f : { A , B } -1-1-> D /\ ph ) )
75 74 ex 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> ( ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) -> ( f : { A , B } -1-1-> D /\ ph ) ) )
76 75 eximdv 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> ( E. f ( f : { A , B } -1-1-> D /\ ( x = ( f ` A ) /\ y = ( f ` B ) ) ) -> E. f ( f : { A , B } -1-1-> D /\ ph ) ) )
77 65 76 mpd 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) /\ ( x =/= y /\ ps ) ) -> E. f ( f : { A , B } -1-1-> D /\ ph ) )
78 77 ex 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( x e. D /\ y e. D ) ) -> ( ( x =/= y /\ ps ) -> E. f ( f : { A , B } -1-1-> D /\ ph ) ) )
79 78 rexlimdvva 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( E. x e. D E. y e. D ( x =/= y /\ ps ) -> E. f ( f : { A , B } -1-1-> D /\ ph ) ) )
80 33 79 impbid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( E. f ( f : { A , B } -1-1-> D /\ ph ) <-> E. x e. D E. y e. D ( x =/= y /\ ps ) ) )