Metamath Proof Explorer

Theorem pmtrfv

Description: General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t 
|- T = ( pmTrsp ` D )
Assertion pmtrfv 
|- ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )

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 2 fveq1d 
 |-  ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( ( T ` P ) ` Z ) = ( ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ` Z ) )
4 3 adantr 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = ( ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ` Z ) )
5 eqid 
 |-  ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) )
6 eleq1 
 |-  ( z = Z -> ( z e. P <-> Z e. P ) )
7 sneq 
 |-  ( z = Z -> { z } = { Z } )
8 7 difeq2d 
 |-  ( z = Z -> ( P \ { z } ) = ( P \ { Z } ) )
9 8 unieqd 
 |-  ( z = Z -> U. ( P \ { z } ) = U. ( P \ { Z } ) )
10 id 
 |-  ( z = Z -> z = Z )
11 6 9 10 ifbieq12d 
 |-  ( z = Z -> if ( z e. P , U. ( P \ { z } ) , z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
12 simpr 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> Z e. D )
13 simpl3 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> P ~~ 2o )
14 relen 
 |-  Rel ~~
15 14 brrelex1i 
 |-  ( P ~~ 2o -> P e. _V )
16 difexg 
 |-  ( P e. _V -> ( P \ { Z } ) e. _V )
17 uniexg 
 |-  ( ( P \ { Z } ) e. _V -> U. ( P \ { Z } ) e. _V )
18 13 15 16 17 4syl 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> U. ( P \ { Z } ) e. _V )
19 ifexg 
 |-  ( ( U. ( P \ { Z } ) e. _V /\ Z e. D ) -> if ( Z e. P , U. ( P \ { Z } ) , Z ) e. _V )
20 18 19 sylancom 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> if ( Z e. P , U. ( P \ { Z } ) , Z ) e. _V )
21 5 11 12 20 fvmptd3 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
22 4 21 eqtrd 
 |-  ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )