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	1	raleqi	⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
4		1ex	⊢ 1 ∈ V
5		2ex	⊢ 2 ∈ V
6		fveq2	⊢ ( 𝑖 = 1 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 1 ) )
7		fveq2	⊢ ( 𝑖 = 1 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 1 ) )
8	6 7	eqeq12d	⊢ ( 𝑖 = 1 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
9		fveq2	⊢ ( 𝑖 = 2 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 2 ) )
10		fveq2	⊢ ( 𝑖 = 2 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 2 ) )
11	9 10	eqeq12d	⊢ ( 𝑖 = 2 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
12	4 5 8 11	ralpr	⊢ ( ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
13	3 12	bitri	⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
14	13	bilanri	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
15		elmapfn	⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 Fn 𝐼 )
16	15 2	eleq2s	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 Fn 𝐼 )
17		elmapfn	⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → 𝑌 Fn 𝐼 )
18	17 2	eleq2s	⊢ ( 𝑌 ∈ 𝑃 → 𝑌 Fn 𝐼 )
19	16 18	anim12i	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) )
20	19	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) )
21		eqfnfv	⊢ ( ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) )
22	20 21	syl	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) )
23	14 22	mpbird	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → 𝑋 = 𝑌 )
24	23	ex	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → 𝑋 = 𝑌 ) )
25	24	necon3ad	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≠ 𝑌 → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) )
26	25	3impia	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
27		neorian	⊢ ( ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ↔ ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
28	26 27	sylibr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )