Metamath Proof Explorer

Theorem pmtrmvd

Description: A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t 
|- T = ( pmTrsp ` D )
Assertion pmtrmvd 
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> dom ( ( T ` P ) \ _I ) = P )

Proof

Step Hyp Ref Expression
1 pmtrfval.t 
 |-  T = ( pmTrsp ` D )
2 1 pmtrf 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) : D --> D )
3 ffn 
 |-  ( ( T ` P ) : D --> D -> ( T ` P ) Fn D )
4 fndifnfp 
 |-  ( ( T ` P ) Fn D -> dom ( ( T ` P ) \ _I ) = { z e. D | ( ( T ` P ) ` z ) =/= z } )
5 2 3 4 3syl 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> dom ( ( T ` P ) \ _I ) = { z e. D | ( ( T ` P ) ` z ) =/= z } )
6 1 pmtrfv 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) -> ( ( T ` P ) ` z ) = if ( z e. P , U. ( P \ { z } ) , z ) )
7 6 neeq1d 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) -> ( ( ( T ` P ) ` z ) =/= z <-> if ( z e. P , U. ( P \ { z } ) , z ) =/= z ) )
8 iffalse 
 |-  ( -. z e. P -> if ( z e. P , U. ( P \ { z } ) , z ) = z )
9 8 necon1ai 
 |-  ( if ( z e. P , U. ( P \ { z } ) , z ) =/= z -> z e. P )
10 iftrue 
 |-  ( z e. P -> if ( z e. P , U. ( P \ { z } ) , z ) = U. ( P \ { z } ) )
11 10 adantl 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> if ( z e. P , U. ( P \ { z } ) , z ) = U. ( P \ { z } ) )
12 1onn 
 |-  1o e. _om
13 simpl3 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> P ~~ 2o )
14 df-2o 
 |-  2o = suc 1o
15 13 14 breqtrdi 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> P ~~ suc 1o )
16 simpr 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> z e. P )
17 dif1en 
 |-  ( ( 1o e. _om /\ P ~~ suc 1o /\ z e. P ) -> ( P \ { z } ) ~~ 1o )
18 12 15 16 17 mp3an2i 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> ( P \ { z } ) ~~ 1o )
19 en1uniel 
 |-  ( ( P \ { z } ) ~~ 1o -> U. ( P \ { z } ) e. ( P \ { z } ) )
20 eldifsni 
 |-  ( U. ( P \ { z } ) e. ( P \ { z } ) -> U. ( P \ { z } ) =/= z )
21 18 19 20 3syl 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> U. ( P \ { z } ) =/= z )
22 11 21 eqnetrd 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. P ) -> if ( z e. P , U. ( P \ { z } ) , z ) =/= z )
23 22 ex 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( z e. P -> if ( z e. P , U. ( P \ { z } ) , z ) =/= z ) )
24 9 23 impbid2 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( if ( z e. P , U. ( P \ { z } ) , z ) =/= z <-> z e. P ) )
25 24 adantr 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) -> ( if ( z e. P , U. ( P \ { z } ) , z ) =/= z <-> z e. P ) )
26 7 25 bitrd 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) -> ( ( ( T ` P ) ` z ) =/= z <-> z e. P ) )
27 26 rabbidva 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> { z e. D | ( ( T ` P ) ` z ) =/= z } = { z e. D | z e. P } )
28 incom 
 |-  ( P i^i D ) = ( D i^i P )
29 dfin5 
 |-  ( D i^i P ) = { z e. D | z e. P }
30 28 29 eqtri 
 |-  ( P i^i D ) = { z e. D | z e. P }
31 27 30 eqtr4di 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> { z e. D | ( ( T ` P ) ` z ) =/= z } = ( P i^i D ) )
32 simp2 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P C_ D )
33 df-ss 
 |-  ( P C_ D <-> ( P i^i D ) = P )
34 32 33 sylib 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( P i^i D ) = P )
35 5 31 34 3eqtrd 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> dom ( ( T ` P ) \ _I ) = P )