Metamath Proof Explorer


Theorem rrx2pnecoorneor

Description: If two different points X and Y in a real Euclidean space of dimension 2 are different, then they are different at least at one coordinate. (Contributed by AV, 26-Feb-2023)

Ref Expression
Hypotheses rrx2pnecoorneor.i
|- I = { 1 , 2 }
rrx2pnecoorneor.b
|- P = ( RR ^m I )
Assertion rrx2pnecoorneor
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) )

Proof

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 ) ) )