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 = (0 ..^2)$
	rrx2pnecoorneor.b	$⊢ P = ℝ^{I}$
Assertion	rrx2pnecoorneor	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (0) \neq Y (0) \lor X (1) \neq Y (1))$

Proof

Step	Hyp	Ref	Expression
1		rrx2pnecoorneor.i	$⊢ I = (0 ..^2)$
2		rrx2pnecoorneor.b	$⊢ P = ℝ^{I}$
3		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
4	1 3	eqtri	$⊢ I = \{0, 1\}$
5	4	raleqi	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow \forall i \in \{0, 1\} X (i) = Y (i)$
6		c0ex	$⊢ 0 \in V$
7		1ex	$⊢ 1 \in V$
8		fveq2	$⊢ i = 0 \to X (i) = X (0)$
9		fveq2	$⊢ i = 0 \to Y (i) = Y (0)$
10	8 9	eqeq12d	$⊢ i = 0 \to (X (i) = Y (i) \leftrightarrow X (0) = Y (0))$
11		fveq2	$⊢ i = 1 \to X (i) = X (1)$
12		fveq2	$⊢ i = 1 \to Y (i) = Y (1)$
13	11 12	eqeq12d	$⊢ i = 1 \to (X (i) = Y (i) \leftrightarrow X (1) = Y (1))$
14	6 7 10 13	ralpr	$⊢ \forall i \in \{0, 1\} X (i) = Y (i) \leftrightarrow (X (0) = Y (0) \land X (1) = Y (1))$
15	5 14	bitri	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow (X (0) = Y (0) \land X (1) = Y (1))$
16	15	bilanri	$⊢ ((X \in P \land Y \in P) \land (X (0) = Y (0) \land X (1) = Y (1))) \to \forall i \in I X (i) = Y (i)$
17		elmapfn	$⊢ X \in (ℝ^{I}) \to X Fn I$
18	17 2	eleq2s	$⊢ X \in P \to X Fn I$
19		elmapfn	$⊢ Y \in (ℝ^{I}) \to Y Fn I$
20	19 2	eleq2s	$⊢ Y \in P \to Y Fn I$
21	18 20	anim12i	$⊢ (X \in P \land Y \in P) \to (X Fn I \land Y Fn I)$
22	21	adantr	$⊢ ((X \in P \land Y \in P) \land (X (0) = Y (0) \land X (1) = Y (1))) \to (X Fn I \land Y Fn I)$
23		eqfnfv	$⊢ (X Fn I \land Y Fn I) \to (X = Y \leftrightarrow \forall i \in I X (i) = Y (i))$
24	22 23	syl	$⊢ ((X \in P \land Y \in P) \land (X (0) = Y (0) \land X (1) = Y (1))) \to (X = Y \leftrightarrow \forall i \in I X (i) = Y (i))$
25	16 24	mpbird	$⊢ ((X \in P \land Y \in P) \land (X (0) = Y (0) \land X (1) = Y (1))) \to X = Y$
26	25	ex	$⊢ (X \in P \land Y \in P) \to ((X (0) = Y (0) \land X (1) = Y (1)) \to X = Y)$
27	26	necon3ad	$⊢ (X \in P \land Y \in P) \to (X \neq Y \to \neg (X (0) = Y (0) \land X (1) = Y (1)))$
28	27	3impia	$⊢ (X \in P \land Y \in P \land X \neq Y) \to \neg (X (0) = Y (0) \land X (1) = Y (1))$
29		neorian	$⊢ (X (0) \neq Y (0) \lor X (1) \neq Y (1)) \leftrightarrow \neg (X (0) = Y (0) \land X (1) = Y (1))$
30	28 29	sylibr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (0) \neq Y (0) \lor X (1) \neq Y (1))$

Metamath Proof Explorer

Theorem rrx2pnecoorneor

Proof