Metamath Proof Explorer

Theorem pmtrf

Description: Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrfval.t 
 |-  T = ( pmTrsp ` D )
2 1 pmtrval 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) )
3 simpll2 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> P C_ D )
4 1onn 
 |-  1o e. _om
5 simpll3 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> P ~~ 2o )
6 df-2o 
 |-  2o = suc 1o
7 5 6 breqtrdi 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> P ~~ suc 1o )
8 simpr 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> z e. P )
9 dif1en 
 |-  ( ( 1o e. _om /\ P ~~ suc 1o /\ z e. P ) -> ( P \ { z } ) ~~ 1o )
10 4 7 8 9 mp3an2i 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> ( P \ { z } ) ~~ 1o )
11 en1uniel 
 |-  ( ( P \ { z } ) ~~ 1o -> U. ( P \ { z } ) e. ( P \ { z } ) )
12 eldifi 
 |-  ( U. ( P \ { z } ) e. ( P \ { z } ) -> U. ( P \ { z } ) e. P )
13 10 11 12 3syl 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> U. ( P \ { z } ) e. P )
14 3 13 sseldd 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ z e. P ) -> U. ( P \ { z } ) e. D )
15 simplr 
 |-  ( ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) /\ -. z e. P ) -> z e. D )
16 14 15 ifclda 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ z e. D ) -> if ( z e. P , U. ( P \ { z } ) , z ) e. D )
17 2 16 fmpt3d 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) : D --> D )