Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( A = <. x , y , z >. -> ( 2nd ` A ) = ( 2nd ` <. x , y , z >. ) ) |
2 |
|
ot3rdg |
|- ( z e. _V -> ( 2nd ` <. x , y , z >. ) = z ) |
3 |
2
|
elv |
|- ( 2nd ` <. x , y , z >. ) = z |
4 |
1 3
|
eqtr2di |
|- ( A = <. x , y , z >. -> z = ( 2nd ` A ) ) |
5 |
|
sbceq1a |
|- ( z = ( 2nd ` A ) -> ( ph <-> [. ( 2nd ` A ) / z ]. ph ) ) |
6 |
4 5
|
syl |
|- ( A = <. x , y , z >. -> ( ph <-> [. ( 2nd ` A ) / z ]. ph ) ) |
7 |
|
2fveq3 |
|- ( A = <. x , y , z >. -> ( 2nd ` ( 1st ` A ) ) = ( 2nd ` ( 1st ` <. x , y , z >. ) ) ) |
8 |
|
vex |
|- x e. _V |
9 |
|
vex |
|- y e. _V |
10 |
|
vex |
|- z e. _V |
11 |
|
ot2ndg |
|- ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( 2nd ` ( 1st ` <. x , y , z >. ) ) = y ) |
12 |
8 9 10 11
|
mp3an |
|- ( 2nd ` ( 1st ` <. x , y , z >. ) ) = y |
13 |
7 12
|
eqtr2di |
|- ( A = <. x , y , z >. -> y = ( 2nd ` ( 1st ` A ) ) ) |
14 |
|
sbceq1a |
|- ( y = ( 2nd ` ( 1st ` A ) ) -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) ) |
15 |
13 14
|
syl |
|- ( A = <. x , y , z >. -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) ) |
16 |
|
2fveq3 |
|- ( A = <. x , y , z >. -> ( 1st ` ( 1st ` A ) ) = ( 1st ` ( 1st ` <. x , y , z >. ) ) ) |
17 |
|
ot1stg |
|- ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( 1st ` ( 1st ` <. x , y , z >. ) ) = x ) |
18 |
8 9 10 17
|
mp3an |
|- ( 1st ` ( 1st ` <. x , y , z >. ) ) = x |
19 |
16 18
|
eqtr2di |
|- ( A = <. x , y , z >. -> x = ( 1st ` ( 1st ` A ) ) ) |
20 |
|
sbceq1a |
|- ( x = ( 1st ` ( 1st ` A ) ) -> ( [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) ) |
21 |
19 20
|
syl |
|- ( A = <. x , y , z >. -> ( [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) ) |
22 |
6 15 21
|
3bitrrd |
|- ( A = <. x , y , z >. -> ( [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> ph ) ) |