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	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	Assertion	prproropf1olem0	⊢ ( 𝑊 ∈ 𝑂 ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2	1	eleq2i	⊢ ( 𝑊 ∈ 𝑂 ↔ 𝑊 ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) )
3		elin	⊢ ( 𝑊 ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ↔ ( 𝑊 ∈ 𝑅 ∧ 𝑊 ∈ ( 𝑉 × 𝑉 ) ) )
4		ancom	⊢ ( ( 𝑊 ∈ 𝑅 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ) ↔ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ∧ 𝑊 ∈ 𝑅 ) )
5		eleq1	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ 𝑅 ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ 𝑅 ) )
6		df-br	⊢ ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ 𝑅 )
7	5 6	bitr4di	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ 𝑅 ↔ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
8	7	adantr	⊢ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) → ( 𝑊 ∈ 𝑅 ↔ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
9	8	pm5.32i	⊢ ( ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ∧ 𝑊 ∈ 𝑅 ) ↔ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
10	4 9	bitri	⊢ ( ( 𝑊 ∈ 𝑅 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ) ↔ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
11		elxp6	⊢ ( 𝑊 ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) )
12	11	anbi2i	⊢ ( ( 𝑊 ∈ 𝑅 ∧ 𝑊 ∈ ( 𝑉 × 𝑉 ) ) ↔ ( 𝑊 ∈ 𝑅 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ) )
13		df-3an	⊢ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ↔ ( ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
14	10 12 13	3bitr4i	⊢ ( ( 𝑊 ∈ 𝑅 ∧ 𝑊 ∈ ( 𝑉 × 𝑉 ) ) ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
15	2 3 14	3bitri	⊢ ( 𝑊 ∈ 𝑂 ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )

Metamath Proof Explorer

Theorem prproropf1olem0

Proof