prproropf1olem0

Description: Lemma 0 for prproropf1o . Remark: O , the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, can alternatively be written as O = { x e. ( V X. V ) | ( 1stx ) R ( 2ndx ) } or even as O = { x e. ( V X. V ) | <. ( 1stx ) , ( 2ndx ) >. e. R } , by which the relationship between ordered and unordered pair is immediately visible. (Contributed by AV, 18-Mar-2023)

		Ref	Expression
	Hypothesis	prproropf1o.o	$⊢ O = R \cap (V \times V)$
	Assertion	prproropf1olem0	$⊢ W \in O \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))$

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	$⊢ O = R \cap (V \times V)$
2	1	eleq2i	$⊢ W \in O \leftrightarrow W \in (R \cap (V \times V))$
3		elin	$⊢ W \in (R \cap (V \times V)) \leftrightarrow (W \in R \land W \in (V \times V))$
4		ancom	$⊢ (W \in R \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V))) \leftrightarrow ((W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \land W \in R)$
5		eleq1	$⊢ W = ⟨1^{st} (W), 2^{nd} (W)⟩ \to (W \in R \leftrightarrow ⟨1^{st} (W), 2^{nd} (W)⟩ \in R)$
6		df-br	$⊢ 1^{st} (W) R 2^{nd} (W) \leftrightarrow ⟨1^{st} (W), 2^{nd} (W)⟩ \in R$
7	5 6	bitr4di	$⊢ W = ⟨1^{st} (W), 2^{nd} (W)⟩ \to (W \in R \leftrightarrow 1^{st} (W) R 2^{nd} (W))$
8	7	adantr	$⊢ (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \to (W \in R \leftrightarrow 1^{st} (W) R 2^{nd} (W))$
9	8	pm5.32i	$⊢ ((W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \land W \in R) \leftrightarrow ((W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \land 1^{st} (W) R 2^{nd} (W))$
10	4 9	bitri	$⊢ (W \in R \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V))) \leftrightarrow ((W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \land 1^{st} (W) R 2^{nd} (W))$
11		elxp6	$⊢ W \in (V \times V) \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V))$
12	11	anbi2i	$⊢ (W \in R \land W \in (V \times V)) \leftrightarrow (W \in R \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)))$
13		df-3an	$⊢ (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W)) \leftrightarrow ((W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \land 1^{st} (W) R 2^{nd} (W))$
14	10 12 13	3bitr4i	$⊢ (W \in R \land W \in (V \times V)) \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))$
15	2 3 14	3bitri	$⊢ W \in O \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))$

Metamath Proof Explorer

Theorem prproropf1olem0

Proof