Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrrn.t |
|- T = ( pmTrsp ` D ) |
2 |
|
pmtrrn.r |
|- R = ran T |
3 |
|
pmtrfrn.p |
|- P = dom ( F \ _I ) |
4 |
1 2 3
|
pmtrfrn |
|- ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) ) |
5 |
4
|
simprd |
|- ( F e. R -> F = ( T ` P ) ) |
6 |
5
|
fveq1d |
|- ( F e. R -> ( F ` Z ) = ( ( T ` P ) ` Z ) ) |
7 |
6
|
adantr |
|- ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = ( ( T ` P ) ` Z ) ) |
8 |
4
|
simpld |
|- ( F e. R -> ( D e. _V /\ P C_ D /\ P ~~ 2o ) ) |
9 |
1
|
pmtrfv |
|- ( ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) ) |
10 |
8 9
|
sylan |
|- ( ( F e. R /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) ) |
11 |
7 10
|
eqtrd |
|- ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) ) |