Metamath Proof Explorer

Theorem f1otrspeq

Description: A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1otrspeq 
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F = G )

Proof

Step Hyp Ref Expression
1 f1ofn 
 |-  ( F : A -1-1-onto-> A -> F Fn A )
2 1 ad2antrr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F Fn A )
3 f1ofn 
 |-  ( G : A -1-1-onto-> A -> G Fn A )
4 3 ad2antlr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> G Fn A )
5 1onn 
 |-  1o e. _om
6 simplrr 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( G \ _I ) = dom ( F \ _I ) )
7 simplrl 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( F \ _I ) ~~ 2o )
8 df-2o 
 |-  2o = suc 1o
9 7 8 breqtrdi 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( F \ _I ) ~~ suc 1o )
10 6 9 eqbrtrd 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( G \ _I ) ~~ suc 1o )
11 simpr 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> x e. dom ( G \ _I ) )
12 dif1en 
 |-  ( ( 1o e. _om /\ dom ( G \ _I ) ~~ suc 1o /\ x e. dom ( G \ _I ) ) -> ( dom ( G \ _I ) \ { x } ) ~~ 1o )
13 5 10 11 12 mp3an2i 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( dom ( G \ _I ) \ { x } ) ~~ 1o )
14 euen1b 
 |-  ( ( dom ( G \ _I ) \ { x } ) ~~ 1o <-> E! y y e. ( dom ( G \ _I ) \ { x } ) )
15 eumo 
 |-  ( E! y y e. ( dom ( G \ _I ) \ { x } ) -> E* y y e. ( dom ( G \ _I ) \ { x } ) )
16 14 15 sylbi 
 |-  ( ( dom ( G \ _I ) \ { x } ) ~~ 1o -> E* y y e. ( dom ( G \ _I ) \ { x } ) )
17 13 16 syl 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> E* y y e. ( dom ( G \ _I ) \ { x } ) )
18 f1omvdmvd 
 |-  ( ( F : A -1-1-onto-> A /\ x e. dom ( F \ _I ) ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) )
19 18 ex 
 |-  ( F : A -1-1-onto-> A -> ( x e. dom ( F \ _I ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) )
20 19 ad2antrr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( F \ _I ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) )
21 eleq2 
 |-  ( dom ( G \ _I ) = dom ( F \ _I ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) )
22 21 ad2antll 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) )
23 difeq1 
 |-  ( dom ( G \ _I ) = dom ( F \ _I ) -> ( dom ( G \ _I ) \ { x } ) = ( dom ( F \ _I ) \ { x } ) )
24 23 eleq2d 
 |-  ( dom ( G \ _I ) = dom ( F \ _I ) -> ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) )
25 24 ad2antll 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) )
26 20 22 25 3imtr4d 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( G \ _I ) -> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) ) )
27 26 imp 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) )
28 f1omvdmvd 
 |-  ( ( G : A -1-1-onto-> A /\ x e. dom ( G \ _I ) ) -> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) )
29 28 ad4ant24 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) )
30 fvex 
 |-  ( F ` x ) e. _V
31 fvex 
 |-  ( G ` x ) e. _V
32 30 31 pm3.2i 
 |-  ( ( F ` x ) e. _V /\ ( G ` x ) e. _V )
33 eleq1 
 |-  ( y = ( F ` x ) -> ( y e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) ) )
34 eleq1 
 |-  ( y = ( G ` x ) -> ( y e. ( dom ( G \ _I ) \ { x } ) <-> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) )
35 33 34 moi 
 |-  ( ( ( ( F ` x ) e. _V /\ ( G ` x ) e. _V ) /\ E* y y e. ( dom ( G \ _I ) \ { x } ) /\ ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) /\ ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) -> ( F ` x ) = ( G ` x ) )
36 32 35 mp3an1 
 |-  ( ( E* y y e. ( dom ( G \ _I ) \ { x } ) /\ ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) /\ ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) -> ( F ` x ) = ( G ` x ) )
37 17 27 29 36 syl12anc 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) )
38 37 adantlr 
 |-  ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) )
39 simplrr 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> dom ( G \ _I ) = dom ( F \ _I ) )
40 39 eleq2d 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) )
41 fnelnfp 
 |-  ( ( F Fn A /\ x e. A ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) )
42 2 41 sylan 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) )
43 40 42 bitrd 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( F ` x ) =/= x ) )
44 43 necon2bbid 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( ( F ` x ) = x <-> -. x e. dom ( G \ _I ) ) )
45 44 biimpar 
 |-  ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( F ` x ) = x )
46 fnelnfp 
 |-  ( ( G Fn A /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( G ` x ) =/= x ) )
47 4 46 sylan 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( G ` x ) =/= x ) )
48 47 necon2bbid 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( ( G ` x ) = x <-> -. x e. dom ( G \ _I ) ) )
49 48 biimpar 
 |-  ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( G ` x ) = x )
50 45 49 eqtr4d 
 |-  ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) )
51 38 50 pm2.61dan 
 |-  ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
52 2 4 51 eqfnfvd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F = G )