Step |
Hyp |
Ref |
Expression |
1 |
|
rrx2pnecoorneor.i |
|- I = { 1 , 2 } |
2 |
|
rrx2pnecoorneor.b |
|- P = ( RR ^m I ) |
3 |
|
simpr |
|- ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) -> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) |
4 |
1
|
raleqi |
|- ( A. i e. I ( X ` i ) = ( Y ` i ) <-> A. i e. { 1 , 2 } ( X ` i ) = ( Y ` i ) ) |
5 |
|
1ex |
|- 1 e. _V |
6 |
|
2ex |
|- 2 e. _V |
7 |
|
fveq2 |
|- ( i = 1 -> ( X ` i ) = ( X ` 1 ) ) |
8 |
|
fveq2 |
|- ( i = 1 -> ( Y ` i ) = ( Y ` 1 ) ) |
9 |
7 8
|
eqeq12d |
|- ( i = 1 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 1 ) = ( Y ` 1 ) ) ) |
10 |
|
fveq2 |
|- ( i = 2 -> ( X ` i ) = ( X ` 2 ) ) |
11 |
|
fveq2 |
|- ( i = 2 -> ( Y ` i ) = ( Y ` 2 ) ) |
12 |
10 11
|
eqeq12d |
|- ( i = 2 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 2 ) = ( Y ` 2 ) ) ) |
13 |
5 6 9 12
|
ralpr |
|- ( A. i e. { 1 , 2 } ( X ` i ) = ( Y ` i ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) |
14 |
4 13
|
bitri |
|- ( A. i e. I ( X ` i ) = ( Y ` i ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) |
15 |
3 14
|
sylibr |
|- ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) -> A. i e. I ( X ` i ) = ( Y ` i ) ) |
16 |
|
elmapfn |
|- ( X e. ( RR ^m I ) -> X Fn I ) |
17 |
16 2
|
eleq2s |
|- ( X e. P -> X Fn I ) |
18 |
|
elmapfn |
|- ( Y e. ( RR ^m I ) -> Y Fn I ) |
19 |
18 2
|
eleq2s |
|- ( Y e. P -> Y Fn I ) |
20 |
17 19
|
anim12i |
|- ( ( X e. P /\ Y e. P ) -> ( X Fn I /\ Y Fn I ) ) |
21 |
20
|
adantr |
|- ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) -> ( X Fn I /\ Y Fn I ) ) |
22 |
|
eqfnfv |
|- ( ( X Fn I /\ Y Fn I ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) ) |
23 |
21 22
|
syl |
|- ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) ) |
24 |
15 23
|
mpbird |
|- ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) -> X = Y ) |
25 |
24
|
ex |
|- ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> X = Y ) ) |
26 |
25
|
necon3ad |
|- ( ( X e. P /\ Y e. P ) -> ( X =/= Y -> -. ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) ) |
27 |
26
|
3impia |
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> -. ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) |
28 |
|
neorian |
|- ( ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) <-> -. ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) ) |
29 |
27 28
|
sylibr |
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) ) |