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 )