Metamath Proof Explorer

Theorem prelrrx2b

Description: Equivalent condition for being one of a pair of points in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

		Ref	Expression
	Hypotheses	prelrrx2.i	$⊢ I = (0 ..^2)$
		prelrrx2.b	$⊢ P = ℝ^{I}$
	Assertion	prelrrx2b	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z \in P \land ((Z (0) = A \land Z (1) = B) \lor (Z (0) = X \land Z (1) = Y))) \leftrightarrow Z \in \{⟨“ A B ”⟩, ⟨“ X Y ”⟩\})$

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	$⊢ I = (0 ..^2)$
2		prelrrx2.b	$⊢ P = ℝ^{I}$
3		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to A \in ℝ$
4		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℝ$
5	3 4	s2cld	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ⟨“ A B ”⟩ \in Word ℝ$
6		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℝ$
7		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to Y \in ℝ$
8	6 7	s2cld	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ⟨“ X Y ”⟩ \in Word ℝ$
9		elpr2g	$⊢ (⟨“ A B ”⟩ \in Word ℝ \land ⟨“ X Y ”⟩ \in Word ℝ) \to (Z \in \{⟨“ A B ”⟩, ⟨“ X Y ”⟩\} \leftrightarrow (Z = ⟨“ A B ”⟩ \lor Z = ⟨“ X Y ”⟩))$
10	5 8 9	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in \{⟨“ A B ”⟩, ⟨“ X Y ”⟩\} \leftrightarrow (Z = ⟨“ A B ”⟩ \lor Z = ⟨“ X Y ”⟩))$
11	1 2 3 4	prelrrx2bd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z = ⟨“ A B ”⟩ \leftrightarrow (Z \in P \land (Z (0) = A \land Z (1) = B)))$
12	1 2 6 7	prelrrx2bd	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z = ⟨“ X Y ”⟩ \leftrightarrow (Z \in P \land (Z (0) = X \land Z (1) = Y)))$
13	11 12	orbi12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z = ⟨“ A B ”⟩ \lor Z = ⟨“ X Y ”⟩) \leftrightarrow ((Z \in P \land (Z (0) = A \land Z (1) = B)) \lor (Z \in P \land (Z (0) = X \land Z (1) = Y))))$
14		andi	$⊢ (Z \in P \land ((Z (0) = A \land Z (1) = B) \lor (Z (0) = X \land Z (1) = Y))) \leftrightarrow ((Z \in P \land (Z (0) = A \land Z (1) = B)) \lor (Z \in P \land (Z (0) = X \land Z (1) = Y)))$
15	13 14	bitr4di	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z = ⟨“ A B ”⟩ \lor Z = ⟨“ X Y ”⟩) \leftrightarrow (Z \in P \land ((Z (0) = A \land Z (1) = B) \lor (Z (0) = X \land Z (1) = Y))))$
16	10 15	bitr2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z \in P \land ((Z (0) = A \land Z (1) = B) \lor (Z (0) = X \land Z (1) = Y))) \leftrightarrow Z \in \{⟨“ A B ”⟩, ⟨“ X Y ”⟩\})$