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 )