| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pmtrprfv2.t |
|- T = ( pmTrsp ` D ) |
| 2 |
|
prcom |
|- { Y , X } = { X , Y } |
| 3 |
2
|
fveq2i |
|- ( T ` { Y , X } ) = ( T ` { X , Y } ) |
| 4 |
3
|
fveq1i |
|- ( ( T ` { Y , X } ) ` Y ) = ( ( T ` { X , Y } ) ` Y ) |
| 5 |
|
ancom |
|- ( ( X e. D /\ Y e. D ) <-> ( Y e. D /\ X e. D ) ) |
| 6 |
|
necom |
|- ( X =/= Y <-> Y =/= X ) |
| 7 |
5 6
|
anbi12i |
|- ( ( ( X e. D /\ Y e. D ) /\ X =/= Y ) <-> ( ( Y e. D /\ X e. D ) /\ Y =/= X ) ) |
| 8 |
|
df-3an |
|- ( ( X e. D /\ Y e. D /\ X =/= Y ) <-> ( ( X e. D /\ Y e. D ) /\ X =/= Y ) ) |
| 9 |
|
df-3an |
|- ( ( Y e. D /\ X e. D /\ Y =/= X ) <-> ( ( Y e. D /\ X e. D ) /\ Y =/= X ) ) |
| 10 |
7 8 9
|
3bitr4i |
|- ( ( X e. D /\ Y e. D /\ X =/= Y ) <-> ( Y e. D /\ X e. D /\ Y =/= X ) ) |
| 11 |
1
|
pmtrprfv |
|- ( ( D e. V /\ ( Y e. D /\ X e. D /\ Y =/= X ) ) -> ( ( T ` { Y , X } ) ` Y ) = X ) |
| 12 |
10 11
|
sylan2b |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { Y , X } ) ` Y ) = X ) |
| 13 |
4 12
|
eqtr3id |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` Y ) = X ) |