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

Proof

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

Metamath Proof Explorer

Theorem rrx2pnecoorneor

Proof