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		simpr	$⊢ ((X \in P \land Y \in P) \land (X (1) = Y (1) \land X (2) = Y (2))) \to (X (1) = Y (1) \land X (2) = Y (2))$
4	1	raleqi	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow \forall i \in \{1, 2\} X (i) = Y (i)$
5		1ex	$⊢ 1 \in V$
6		2ex	$⊢ 2 \in V$
7		fveq2	$⊢ i = 1 \to X (i) = X (1)$
8		fveq2	$⊢ i = 1 \to Y (i) = Y (1)$
9	7 8	eqeq12d	$⊢ i = 1 \to (X (i) = Y (i) \leftrightarrow X (1) = Y (1))$
10		fveq2	$⊢ i = 2 \to X (i) = X (2)$
11		fveq2	$⊢ i = 2 \to Y (i) = Y (2)$
12	10 11	eqeq12d	$⊢ i = 2 \to (X (i) = Y (i) \leftrightarrow X (2) = Y (2))$
13	5 6 9 12	ralpr	$⊢ \forall i \in \{1, 2\} X (i) = Y (i) \leftrightarrow (X (1) = Y (1) \land X (2) = Y (2))$
14	4 13	bitri	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow (X (1) = Y (1) \land X (2) = Y (2))$
15	3 14	sylibr	$⊢ ((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)$
16		elmapfn	$⊢ X \in (ℝ^{I}) \to X Fn I$
17	16 2	eleq2s	$⊢ X \in P \to X Fn I$
18		elmapfn	$⊢ Y \in (ℝ^{I}) \to Y Fn I$
19	18 2	eleq2s	$⊢ Y \in P \to Y Fn I$
20	17 19	anim12i	$⊢ (X \in P \land Y \in P) \to (X Fn I \land Y Fn I)$
21	20	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)$
22		eqfnfv	$⊢ (X Fn I \land Y Fn I) \to (X = Y \leftrightarrow \forall i \in I X (i) = Y (i))$
23	21 22	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))$
24	15 23	mpbird	$⊢ ((X \in P \land Y \in P) \land (X (1) = Y (1) \land X (2) = Y (2))) \to X = Y$
25	24	ex	$⊢ (X \in P \land Y \in P) \to ((X (1) = Y (1) \land X (2) = Y (2)) \to X = Y)$
26	25	necon3ad	$⊢ (X \in P \land Y \in P) \to (X \neq Y \to \neg (X (1) = Y (1) \land X (2) = Y (2)))$
27	26	3impia	$⊢ (X \in P \land Y \in P \land X \neq Y) \to \neg (X (1) = Y (1) \land X (2) = Y (2))$
28		neorian	$⊢ (X (1) \neq Y (1) \lor X (2) \neq Y (2)) \leftrightarrow \neg (X (1) = Y (1) \land X (2) = Y (2))$
29	27 28	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