Step |
Hyp |
Ref |
Expression |
1 |
|
xp1st |
|- ( A e. ( ( U X. V ) X. W ) -> ( 1st ` A ) e. ( U X. V ) ) |
2 |
1
|
ad2antrl |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( 1st ` A ) e. ( U X. V ) ) |
3 |
|
3simpa |
|- ( ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) -> ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y ) ) |
4 |
3
|
adantl |
|- ( ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) -> ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y ) ) |
5 |
4
|
adantl |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y ) ) |
6 |
|
eqopi |
|- ( ( ( 1st ` A ) e. ( U X. V ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y ) ) -> ( 1st ` A ) = <. X , Y >. ) |
7 |
2 5 6
|
syl2anc |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( 1st ` A ) = <. X , Y >. ) |
8 |
|
simprr3 |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( 2nd ` A ) = Z ) |
9 |
7 8
|
jca |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( ( 1st ` A ) = <. X , Y >. /\ ( 2nd ` A ) = Z ) ) |
10 |
|
df-ot |
|- <. X , Y , Z >. = <. <. X , Y >. , Z >. |
11 |
10
|
eqeq2i |
|- ( A = <. X , Y , Z >. <-> A = <. <. X , Y >. , Z >. ) |
12 |
|
eqop |
|- ( A e. ( ( U X. V ) X. W ) -> ( A = <. <. X , Y >. , Z >. <-> ( ( 1st ` A ) = <. X , Y >. /\ ( 2nd ` A ) = Z ) ) ) |
13 |
11 12
|
syl5bb |
|- ( A e. ( ( U X. V ) X. W ) -> ( A = <. X , Y , Z >. <-> ( ( 1st ` A ) = <. X , Y >. /\ ( 2nd ` A ) = Z ) ) ) |
14 |
13
|
ad2antrl |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> ( A = <. X , Y , Z >. <-> ( ( 1st ` A ) = <. X , Y >. /\ ( 2nd ` A ) = Z ) ) ) |
15 |
9 14
|
mpbird |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) -> A = <. X , Y , Z >. ) |
16 |
|
opelxpi |
|- ( ( X e. U /\ Y e. V ) -> <. X , Y >. e. ( U X. V ) ) |
17 |
16
|
3adant3 |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> <. X , Y >. e. ( U X. V ) ) |
18 |
|
simp3 |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> Z e. W ) |
19 |
17 18
|
opelxpd |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> <. <. X , Y >. , Z >. e. ( ( U X. V ) X. W ) ) |
20 |
10 19
|
eqeltrid |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> <. X , Y , Z >. e. ( ( U X. V ) X. W ) ) |
21 |
20
|
adantr |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> <. X , Y , Z >. e. ( ( U X. V ) X. W ) ) |
22 |
|
eleq1 |
|- ( A = <. X , Y , Z >. -> ( A e. ( ( U X. V ) X. W ) <-> <. X , Y , Z >. e. ( ( U X. V ) X. W ) ) ) |
23 |
22
|
adantl |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( A e. ( ( U X. V ) X. W ) <-> <. X , Y , Z >. e. ( ( U X. V ) X. W ) ) ) |
24 |
21 23
|
mpbird |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> A e. ( ( U X. V ) X. W ) ) |
25 |
|
2fveq3 |
|- ( A = <. X , Y , Z >. -> ( 1st ` ( 1st ` A ) ) = ( 1st ` ( 1st ` <. X , Y , Z >. ) ) ) |
26 |
|
ot1stg |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( 1st ` ( 1st ` <. X , Y , Z >. ) ) = X ) |
27 |
25 26
|
sylan9eqr |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( 1st ` ( 1st ` A ) ) = X ) |
28 |
|
2fveq3 |
|- ( A = <. X , Y , Z >. -> ( 2nd ` ( 1st ` A ) ) = ( 2nd ` ( 1st ` <. X , Y , Z >. ) ) ) |
29 |
|
ot2ndg |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( 2nd ` ( 1st ` <. X , Y , Z >. ) ) = Y ) |
30 |
28 29
|
sylan9eqr |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( 2nd ` ( 1st ` A ) ) = Y ) |
31 |
|
fveq2 |
|- ( A = <. X , Y , Z >. -> ( 2nd ` A ) = ( 2nd ` <. X , Y , Z >. ) ) |
32 |
|
ot3rdg |
|- ( Z e. W -> ( 2nd ` <. X , Y , Z >. ) = Z ) |
33 |
32
|
3ad2ant3 |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( 2nd ` <. X , Y , Z >. ) = Z ) |
34 |
31 33
|
sylan9eqr |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( 2nd ` A ) = Z ) |
35 |
27 30 34
|
3jca |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) |
36 |
24 35
|
jca |
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ A = <. X , Y , Z >. ) -> ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) ) |
37 |
15 36
|
impbida |
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) <-> A = <. X , Y , Z >. ) ) |