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 )