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	⊢ 𝐼 = ( 0 ..^ 2 )
	rrx2pnecoorneor.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion	rrx2pnecoorneor	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 0 ) ≠ ( 𝑌 ‘ 0 ) ∨ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) )

Proof

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