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 𝐼 = { 1 , 2 }
rrx2pnecoorneor.b 𝑃 = ( ℝ ↑m 𝐼 )
Assertion rrx2pnecoorneor ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i 𝐼 = { 1 , 2 }
2 rrx2pnecoorneor.b 𝑃 = ( ℝ ↑m 𝐼 )
3 simpr ( ( ( 𝑋𝑃𝑌𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
4 1 raleqi ( ∀ 𝑖𝐼 ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ↔ ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋𝑖 ) = ( 𝑌𝑖 ) )
5 1ex 1 ∈ V
6 2ex 2 ∈ V
7 fveq2 ( 𝑖 = 1 → ( 𝑋𝑖 ) = ( 𝑋 ‘ 1 ) )
8 fveq2 ( 𝑖 = 1 → ( 𝑌𝑖 ) = ( 𝑌 ‘ 1 ) )
9 7 8 eqeq12d ( 𝑖 = 1 → ( ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
10 fveq2 ( 𝑖 = 2 → ( 𝑋𝑖 ) = ( 𝑋 ‘ 2 ) )
11 fveq2 ( 𝑖 = 2 → ( 𝑌𝑖 ) = ( 𝑌 ‘ 2 ) )
12 10 11 eqeq12d ( 𝑖 = 2 → ( ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
13 5 6 9 12 ralpr ( ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
14 4 13 bitri ( ∀ 𝑖𝐼 ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
15 3 14 sylibr ( ( ( 𝑋𝑃𝑌𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ∀ 𝑖𝐼 ( 𝑋𝑖 ) = ( 𝑌𝑖 ) )
16 elmapfn ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 Fn 𝐼 )
17 16 2 eleq2s ( 𝑋𝑃𝑋 Fn 𝐼 )
18 elmapfn ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → 𝑌 Fn 𝐼 )
19 18 2 eleq2s ( 𝑌𝑃𝑌 Fn 𝐼 )
20 17 19 anim12i ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑋 Fn 𝐼𝑌 Fn 𝐼 ) )
21 20 adantr ( ( ( 𝑋𝑃𝑌𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 Fn 𝐼𝑌 Fn 𝐼 ) )
22 eqfnfv ( ( 𝑋 Fn 𝐼𝑌 Fn 𝐼 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖𝐼 ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ) )
23 21 22 syl ( ( ( 𝑋𝑃𝑌𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖𝐼 ( 𝑋𝑖 ) = ( 𝑌𝑖 ) ) )
24 15 23 mpbird ( ( ( 𝑋𝑃𝑌𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → 𝑋 = 𝑌 )
25 24 ex ( ( 𝑋𝑃𝑌𝑃 ) → ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → 𝑋 = 𝑌 ) )
26 25 necon3ad ( ( 𝑋𝑃𝑌𝑃 ) → ( 𝑋𝑌 → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) )
27 26 3impia ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
28 neorian ( ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ↔ ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
29 27 28 sylibr ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )