This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtrrn

Description: Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrrn.t 
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r 
 |-  R = ran T
3 mptexg 
 |-  ( D e. V -> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V )
4 3 ralrimivw 
 |-  ( D e. V -> A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V )
5 4 3ad2ant1 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V )
6 eqid 
 |-  ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) )
7 6 fnmpt 
 |-  ( A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V -> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } )
8 5 7 syl 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } )
9 1 pmtrfval 
 |-  ( D e. V -> T = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) )
10 9 3ad2ant1 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> T = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) )
11 10 fneq1d 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T Fn { x e. ~P D | x ~~ 2o } <-> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } ) )
12 8 11 mpbird 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> T Fn { x e. ~P D | x ~~ 2o } )
13 breq1 
 |-  ( x = P -> ( x ~~ 2o <-> P ~~ 2o ) )
14 elpw2g 
 |-  ( D e. V -> ( P e. ~P D <-> P C_ D ) )
15 14 biimpar 
 |-  ( ( D e. V /\ P C_ D ) -> P e. ~P D )
16 15 3adant3 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. ~P D )
17 simp3 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P ~~ 2o )
18 13 16 17 elrabd 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. { x e. ~P D | x ~~ 2o } )
19 fnfvelrn 
 |-  ( ( T Fn { x e. ~P D | x ~~ 2o } /\ P e. { x e. ~P D | x ~~ 2o } ) -> ( T ` P ) e. ran T )
20 12 18 19 syl2anc 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) e. ran T )
21 20 2 eleqtrrdi 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) e. R )