| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pmtrfval.t |
|- T = ( pmTrsp ` D ) |
| 2 |
|
simp1 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> D e. V ) |
| 3 |
|
simp1 |
|- ( ( X e. D /\ Y e. D /\ Z e. D ) -> X e. D ) |
| 4 |
3
|
3ad2ant2 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> X e. D ) |
| 5 |
|
simp22 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Y e. D ) |
| 6 |
4 5
|
prssd |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } C_ D ) |
| 7 |
|
enpr2 |
|- ( ( X e. D /\ Y e. D /\ X =/= Y ) -> { X , Y } ~~ 2o ) |
| 8 |
7
|
3expia |
|- ( ( X e. D /\ Y e. D ) -> ( X =/= Y -> { X , Y } ~~ 2o ) ) |
| 9 |
8
|
3adant3 |
|- ( ( X e. D /\ Y e. D /\ Z e. D ) -> ( X =/= Y -> { X , Y } ~~ 2o ) ) |
| 10 |
9
|
com12 |
|- ( X =/= Y -> ( ( X e. D /\ Y e. D /\ Z e. D ) -> { X , Y } ~~ 2o ) ) |
| 11 |
10
|
3ad2ant1 |
|- ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( ( X e. D /\ Y e. D /\ Z e. D ) -> { X , Y } ~~ 2o ) ) |
| 12 |
11
|
impcom |
|- ( ( ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } ~~ 2o ) |
| 13 |
12
|
3adant1 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } ~~ 2o ) |
| 14 |
|
simp23 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z e. D ) |
| 15 |
1
|
pmtrfv |
|- ( ( ( D e. V /\ { X , Y } C_ D /\ { X , Y } ~~ 2o ) /\ Z e. D ) -> ( ( T ` { X , Y } ) ` Z ) = if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) ) |
| 16 |
2 6 13 14 15
|
syl31anc |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) ) |
| 17 |
|
necom |
|- ( X =/= Z <-> Z =/= X ) |
| 18 |
17
|
biimpi |
|- ( X =/= Z -> Z =/= X ) |
| 19 |
18
|
3ad2ant2 |
|- ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Z =/= X ) |
| 20 |
19
|
3ad2ant3 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z =/= X ) |
| 21 |
|
necom |
|- ( Y =/= Z <-> Z =/= Y ) |
| 22 |
21
|
biimpi |
|- ( Y =/= Z -> Z =/= Y ) |
| 23 |
22
|
3ad2ant3 |
|- ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Z =/= Y ) |
| 24 |
23
|
3ad2ant3 |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z =/= Y ) |
| 25 |
20 24
|
nelprd |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> -. Z e. { X , Y } ) |
| 26 |
25
|
iffalsed |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) = Z ) |
| 27 |
16 26
|
eqtrd |
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = Z ) |