Metamath Proof Explorer

Theorem pmtrfrn

Description: A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t 
|- T = ( pmTrsp ` D )
pmtrrn.r 
|- R = ran T
pmtrfrn.p 
|- P = dom ( F \ _I )
Assertion pmtrfrn 
|- ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r 
 |-  R = ran T
3 pmtrfrn.p 
 |-  P = dom ( F \ _I )
4 noel 
 |-  -. F e. (/)
5 1 rnfvprc 
 |-  ( -. D e. _V -> ran T = (/) )
6 2 5 syl5eq 
 |-  ( -. D e. _V -> R = (/) )
7 6 eleq2d 
 |-  ( -. D e. _V -> ( F e. R <-> F e. (/) ) )
8 4 7 mtbiri 
 |-  ( -. D e. _V -> -. F e. R )
9 8 con4i 
 |-  ( F e. R -> D e. _V )
10 mptexg 
 |-  ( D e. _V -> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) e. _V )
11 10 ralrimivw 
 |-  ( D e. _V -> A. w e. { x e. ~P D | x ~~ 2o } ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) e. _V )
12 eqid 
 |-  ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) ) = ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) )
13 12 fnmpt 
 |-  ( A. w e. { x e. ~P D | x ~~ 2o } ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) e. _V -> ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) ) Fn { x e. ~P D | x ~~ 2o } )
14 11 13 syl 
 |-  ( D e. _V -> ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) ) Fn { x e. ~P D | x ~~ 2o } )
15 1 pmtrfval 
 |-  ( D e. _V -> T = ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) ) )
16 15 fneq1d 
 |-  ( D e. _V -> ( T Fn { x e. ~P D | x ~~ 2o } <-> ( w e. { x e. ~P D | x ~~ 2o } |-> ( z e. D |-> if ( z e. w , U. ( w \ { z } ) , z ) ) ) Fn { x e. ~P D | x ~~ 2o } ) )
17 14 16 mpbird 
 |-  ( D e. _V -> T Fn { x e. ~P D | x ~~ 2o } )
18 fvelrnb 
 |-  ( T Fn { x e. ~P D | x ~~ 2o } -> ( F e. ran T <-> E. y e. { x e. ~P D | x ~~ 2o } ( T ` y ) = F ) )
19 17 18 syl 
 |-  ( D e. _V -> ( F e. ran T <-> E. y e. { x e. ~P D | x ~~ 2o } ( T ` y ) = F ) )
20 2 eleq2i 
 |-  ( F e. R <-> F e. ran T )
21 breq1 
 |-  ( x = y -> ( x ~~ 2o <-> y ~~ 2o ) )
22 21 rexrab 
 |-  ( E. y e. { x e. ~P D | x ~~ 2o } ( T ` y ) = F <-> E. y e. ~P D ( y ~~ 2o /\ ( T ` y ) = F ) )
23 22 bicomi 
 |-  ( E. y e. ~P D ( y ~~ 2o /\ ( T ` y ) = F ) <-> E. y e. { x e. ~P D | x ~~ 2o } ( T ` y ) = F )
24 19 20 23 3bitr4g 
 |-  ( D e. _V -> ( F e. R <-> E. y e. ~P D ( y ~~ 2o /\ ( T ` y ) = F ) ) )
25 elpwi 
 |-  ( y e. ~P D -> y C_ D )
26 simp1 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> D e. _V )
27 1 pmtrmvd 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> dom ( ( T ` y ) \ _I ) = y )
28 simp2 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> y C_ D )
29 27 28 eqsstrd 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> dom ( ( T ` y ) \ _I ) C_ D )
30 simp3 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> y ~~ 2o )
31 27 30 eqbrtrd 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> dom ( ( T ` y ) \ _I ) ~~ 2o )
32 26 29 31 3jca 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) )
33 27 eqcomd 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> y = dom ( ( T ` y ) \ _I ) )
34 33 fveq2d 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> ( T ` y ) = ( T ` dom ( ( T ` y ) \ _I ) ) )
35 32 34 jca 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> ( ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) /\ ( T ` y ) = ( T ` dom ( ( T ` y ) \ _I ) ) ) )
36 difeq1 
 |-  ( ( T ` y ) = F -> ( ( T ` y ) \ _I ) = ( F \ _I ) )
37 36 dmeqd 
 |-  ( ( T ` y ) = F -> dom ( ( T ` y ) \ _I ) = dom ( F \ _I ) )
38 37 3 eqtr4di 
 |-  ( ( T ` y ) = F -> dom ( ( T ` y ) \ _I ) = P )
39 sseq1 
 |-  ( dom ( ( T ` y ) \ _I ) = P -> ( dom ( ( T ` y ) \ _I ) C_ D <-> P C_ D ) )
40 breq1 
 |-  ( dom ( ( T ` y ) \ _I ) = P -> ( dom ( ( T ` y ) \ _I ) ~~ 2o <-> P ~~ 2o ) )
41 39 40 3anbi23d 
 |-  ( dom ( ( T ` y ) \ _I ) = P -> ( ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) <-> ( D e. _V /\ P C_ D /\ P ~~ 2o ) ) )
42 41 adantl 
 |-  ( ( ( T ` y ) = F /\ dom ( ( T ` y ) \ _I ) = P ) -> ( ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) <-> ( D e. _V /\ P C_ D /\ P ~~ 2o ) ) )
43 simpl 
 |-  ( ( ( T ` y ) = F /\ dom ( ( T ` y ) \ _I ) = P ) -> ( T ` y ) = F )
44 fveq2 
 |-  ( dom ( ( T ` y ) \ _I ) = P -> ( T ` dom ( ( T ` y ) \ _I ) ) = ( T ` P ) )
45 44 adantl 
 |-  ( ( ( T ` y ) = F /\ dom ( ( T ` y ) \ _I ) = P ) -> ( T ` dom ( ( T ` y ) \ _I ) ) = ( T ` P ) )
46 43 45 eqeq12d 
 |-  ( ( ( T ` y ) = F /\ dom ( ( T ` y ) \ _I ) = P ) -> ( ( T ` y ) = ( T ` dom ( ( T ` y ) \ _I ) ) <-> F = ( T ` P ) ) )
47 42 46 anbi12d 
 |-  ( ( ( T ` y ) = F /\ dom ( ( T ` y ) \ _I ) = P ) -> ( ( ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) /\ ( T ` y ) = ( T ` dom ( ( T ` y ) \ _I ) ) ) <-> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) )
48 38 47 mpdan 
 |-  ( ( T ` y ) = F -> ( ( ( D e. _V /\ dom ( ( T ` y ) \ _I ) C_ D /\ dom ( ( T ` y ) \ _I ) ~~ 2o ) /\ ( T ` y ) = ( T ` dom ( ( T ` y ) \ _I ) ) ) <-> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) )
49 35 48 syl5ibcom 
 |-  ( ( D e. _V /\ y C_ D /\ y ~~ 2o ) -> ( ( T ` y ) = F -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) )
50 49 3exp 
 |-  ( D e. _V -> ( y C_ D -> ( y ~~ 2o -> ( ( T ` y ) = F -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) ) ) )
51 50 imp4a 
 |-  ( D e. _V -> ( y C_ D -> ( ( y ~~ 2o /\ ( T ` y ) = F ) -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) ) )
52 25 51 syl5 
 |-  ( D e. _V -> ( y e. ~P D -> ( ( y ~~ 2o /\ ( T ` y ) = F ) -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) ) )
53 52 rexlimdv 
 |-  ( D e. _V -> ( E. y e. ~P D ( y ~~ 2o /\ ( T ` y ) = F ) -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) )
54 24 53 sylbid 
 |-  ( D e. _V -> ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) )
55 9 54 mpcom 
 |-  ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) )