Theorem prproropen

Description: The set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, are equinumerous. (Contributed by AV, 15-Mar-2023)

	Ref	Expression
Hypotheses	prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
Assertion	prproropen	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → 𝑂 ≈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3		pwexg	⊢ ( 𝑉 ∈ 𝑊 → 𝒫 𝑉 ∈ V )
4	2 3	rabexd	⊢ ( 𝑉 ∈ 𝑊 → 𝑃 ∈ V )
5	4	adantr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → 𝑃 ∈ V )
6	5	mptexd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ∈ V )
7		eqid	⊢ ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
8	1 2 7	prproropf1o	⊢ ( 𝑅 Or 𝑉 → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) : 𝑃 –1-1-onto→ 𝑂 )
9	8	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) : 𝑃 –1-1-onto→ 𝑂 )
10		f1oeq1	⊢ ( 𝑓 = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) → ( 𝑓 : 𝑃 –1-1-onto→ 𝑂 ↔ ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) : 𝑃 –1-1-onto→ 𝑂 ) )
11	6 9 10	spcedv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑂 )
12		ensymb	⊢ ( 𝑂 ≈ 𝑃 ↔ 𝑃 ≈ 𝑂 )
13		bren	⊢ ( 𝑃 ≈ 𝑂 ↔ ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑂 )
14	12 13	bitri	⊢ ( 𝑂 ≈ 𝑃 ↔ ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑂 )
15	11 14	sylibr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉 ) → 𝑂 ≈ 𝑃 )