Metamath Proof Explorer

Theorem trsp2cyc

Description: Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023)

Ref Expression
Hypotheses trsp2cyc.t 
|- T = ran ( pmTrsp ` D )
trsp2cyc.c 
|- C = ( toCyc ` D )
Assertion trsp2cyc 
|- ( ( D e. V /\ P e. T ) -> E. i e. D E. j e. D ( i =/= j /\ P = ( C ` <" i j "> ) ) )

Proof

Step Hyp Ref Expression
1 trsp2cyc.t 
 |-  T = ran ( pmTrsp ` D )
2 trsp2cyc.c 
 |-  C = ( toCyc ` D )
3 simplr 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> p e. { y e. ~P D | y ~~ 2o } )
4 breq1 
 |-  ( y = p -> ( y ~~ 2o <-> p ~~ 2o ) )
5 4 elrab 
 |-  ( p e. { y e. ~P D | y ~~ 2o } <-> ( p e. ~P D /\ p ~~ 2o ) )
6 3 5 sylib 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> ( p e. ~P D /\ p ~~ 2o ) )
7 6 simprd 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> p ~~ 2o )
8 en2 
 |-  ( p ~~ 2o -> E. i E. j p = { i , j } )
9 7 8 syl 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> E. i E. j p = { i , j } )
10 6 simpld 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> p e. ~P D )
11 10 elpwid 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> p C_ D )
12 11 adantr 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> p C_ D )
13 vex 
 |-  i e. _V
14 13 prid1 
 |-  i e. { i , j }
15 simpr 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> p = { i , j } )
16 14 15 eleqtrrid 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> i e. p )
17 12 16 sseldd 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> i e. D )
18 vex 
 |-  j e. _V
19 18 prid2 
 |-  j e. { i , j }
20 19 15 eleqtrrid 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> j e. p )
21 12 20 sseldd 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> j e. D )
22 7 adantr 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> p ~~ 2o )
23 15 22 eqbrtrrd 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> { i , j } ~~ 2o )
24 pr2ne 
 |-  ( ( i e. D /\ j e. D ) -> ( { i , j } ~~ 2o <-> i =/= j ) )
25 24 biimpa 
 |-  ( ( ( i e. D /\ j e. D ) /\ { i , j } ~~ 2o ) -> i =/= j )
26 17 21 23 25 syl21anc 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> i =/= j )
27 simplr 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
28 simp-4l 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> D e. V )
29 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
30 29 pmtrval 
 |-  ( ( D e. V /\ p C_ D /\ p ~~ 2o ) -> ( ( pmTrsp ` D ) ` p ) = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
31 28 12 22 30 syl3anc 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> ( ( pmTrsp ` D ) ` p ) = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
32 15 fveq2d 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> ( ( pmTrsp ` D ) ` p ) = ( ( pmTrsp ` D ) ` { i , j } ) )
33 27 31 32 3eqtr2d 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> P = ( ( pmTrsp ` D ) ` { i , j } ) )
34 2 28 17 21 26 29 cycpm2tr 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> ( C ` <" i j "> ) = ( ( pmTrsp ` D ) ` { i , j } ) )
35 33 34 eqtr4d 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> P = ( C ` <" i j "> ) )
36 26 35 jca 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> ( i =/= j /\ P = ( C ` <" i j "> ) ) )
37 17 21 36 jca31 
 |-  ( ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) /\ p = { i , j } ) -> ( ( i e. D /\ j e. D ) /\ ( i =/= j /\ P = ( C ` <" i j "> ) ) ) )
38 37 ex 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> ( p = { i , j } -> ( ( i e. D /\ j e. D ) /\ ( i =/= j /\ P = ( C ` <" i j "> ) ) ) ) )
39 38 2eximdv 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> ( E. i E. j p = { i , j } -> E. i E. j ( ( i e. D /\ j e. D ) /\ ( i =/= j /\ P = ( C ` <" i j "> ) ) ) ) )
40 9 39 mpd 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> E. i E. j ( ( i e. D /\ j e. D ) /\ ( i =/= j /\ P = ( C ` <" i j "> ) ) ) )
41 r2ex 
 |-  ( E. i e. D E. j e. D ( i =/= j /\ P = ( C ` <" i j "> ) ) <-> E. i E. j ( ( i e. D /\ j e. D ) /\ ( i =/= j /\ P = ( C ` <" i j "> ) ) ) )
42 40 41 sylibr 
 |-  ( ( ( ( D e. V /\ P e. T ) /\ p e. { y e. ~P D | y ~~ 2o } ) /\ P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> E. i e. D E. j e. D ( i =/= j /\ P = ( C ` <" i j "> ) ) )
43 simpr 
 |-  ( ( D e. V /\ P e. T ) -> P e. T )
44 29 pmtrfval 
 |-  ( D e. V -> ( pmTrsp ` D ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
45 44 adantr 
 |-  ( ( D e. V /\ P e. T ) -> ( pmTrsp ` D ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
46 45 rneqd 
 |-  ( ( D e. V /\ P e. T ) -> ran ( pmTrsp ` D ) = ran ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
47 1 46 eqtrid 
 |-  ( ( D e. V /\ P e. T ) -> T = ran ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
48 43 47 eleqtrd 
 |-  ( ( D e. V /\ P e. T ) -> P e. ran ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
49 eqid 
 |-  ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
50 49 elrnmpt 
 |-  ( P e. T -> ( P e. ran ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) <-> E. p e. { y e. ~P D | y ~~ 2o } P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
51 50 adantl 
 |-  ( ( D e. V /\ P e. T ) -> ( P e. ran ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) <-> E. p e. { y e. ~P D | y ~~ 2o } P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
52 48 51 mpbid 
 |-  ( ( D e. V /\ P e. T ) -> E. p e. { y e. ~P D | y ~~ 2o } P = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
53 42 52 r19.29a 
 |-  ( ( D e. V /\ P e. T ) -> E. i e. D E. j e. D ( i =/= j /\ P = ( C ` <" i j "> ) ) )