Theorem prproropf1o

Description: There is a bijection between 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. (Contributed by AV, 15-Mar-2023)

	Ref	Expression
Hypotheses	prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
	prproropf1o.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
Assertion	prproropf1o	⊢ ( 𝑅 Or 𝑉 → 𝐹 : 𝑃 –1-1-onto→ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3		prproropf1o.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
4	1 2	prproropf1olem2	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑃 ) → ⟨ inf ( 𝑤 , 𝑉 , 𝑅 ) , sup ( 𝑤 , 𝑉 , 𝑅 ) ⟩ ∈ 𝑂 )
5		infeq1	⊢ ( 𝑝 = 𝑤 → inf ( 𝑝 , 𝑉 , 𝑅 ) = inf ( 𝑤 , 𝑉 , 𝑅 ) )
6		supeq1	⊢ ( 𝑝 = 𝑤 → sup ( 𝑝 , 𝑉 , 𝑅 ) = sup ( 𝑤 , 𝑉 , 𝑅 ) )
7	5 6	opeq12d	⊢ ( 𝑝 = 𝑤 → ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ = ⟨ inf ( 𝑤 , 𝑉 , 𝑅 ) , sup ( 𝑤 , 𝑉 , 𝑅 ) ⟩ )
8	7	cbvmptv	⊢ ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) = ( 𝑤 ∈ 𝑃 ↦ ⟨ inf ( 𝑤 , 𝑉 , 𝑅 ) , sup ( 𝑤 , 𝑉 , 𝑅 ) ⟩ )
9	3 8	eqtri	⊢ 𝐹 = ( 𝑤 ∈ 𝑃 ↦ ⟨ inf ( 𝑤 , 𝑉 , 𝑅 ) , sup ( 𝑤 , 𝑉 , 𝑅 ) ⟩ )
10	4 9	fmptd	⊢ ( 𝑅 Or 𝑉 → 𝐹 : 𝑃 ⟶ 𝑂 )
11		3ancomb	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ↔ ( 𝑅 Or 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) )
12		3anass	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) ↔ ( 𝑅 Or 𝑉 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) ) )
13	11 12	bitri	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ↔ ( 𝑅 Or 𝑉 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) ) )
14	1 2 3	prproropf1olem4	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
15	13 14	sylbir	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
16	15	ralrimivva	⊢ ( 𝑅 Or 𝑉 → ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝑃 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
17		dff13	⊢ ( 𝐹 : 𝑃 –1-1→ 𝑂 ↔ ( 𝐹 : 𝑃 ⟶ 𝑂 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝑃 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
18	10 16 17	sylanbrc	⊢ ( 𝑅 Or 𝑉 → 𝐹 : 𝑃 –1-1→ 𝑂 )
19	1 2	prproropf1olem1	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) → { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ∈ 𝑃 )
20		fveq2	⊢ ( 𝑧 = { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) )
21	20	eqeq2d	⊢ ( 𝑧 = { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } → ( 𝑤 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑤 = ( 𝐹 ‘ { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) ) )
22	21	adantl	⊢ ( ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) ∧ 𝑧 = { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) → ( 𝑤 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑤 = ( 𝐹 ‘ { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) ) )
23	1 2 3	prproropf1olem3	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) → ( 𝐹 ‘ { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) = ⟨ ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) ⟩ )
24	1	prproropf1olem0	⊢ ( 𝑤 ∈ 𝑂 ↔ ( 𝑤 = ⟨ ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) ⟩ ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝑉 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝑉 ) ∧ ( 1st ‘ 𝑤 ) 𝑅 ( 2nd ‘ 𝑤 ) ) )
25	24	simp1bi	⊢ ( 𝑤 ∈ 𝑂 → 𝑤 = ⟨ ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) ⟩ )
26	25	eqcomd	⊢ ( 𝑤 ∈ 𝑂 → ⟨ ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) ⟩ = 𝑤 )
27	26	adantl	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) → ⟨ ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) ⟩ = 𝑤 )
28	23 27	eqtr2d	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) → 𝑤 = ( 𝐹 ‘ { ( 1st ‘ 𝑤 ) , ( 2nd ‘ 𝑤 ) } ) )
29	19 22 28	rspcedvd	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑤 ∈ 𝑂 ) → ∃ 𝑧 ∈ 𝑃 𝑤 = ( 𝐹 ‘ 𝑧 ) )
30	29	ralrimiva	⊢ ( 𝑅 Or 𝑉 → ∀ 𝑤 ∈ 𝑂 ∃ 𝑧 ∈ 𝑃 𝑤 = ( 𝐹 ‘ 𝑧 ) )
31		dffo3	⊢ ( 𝐹 : 𝑃 –onto→ 𝑂 ↔ ( 𝐹 : 𝑃 ⟶ 𝑂 ∧ ∀ 𝑤 ∈ 𝑂 ∃ 𝑧 ∈ 𝑃 𝑤 = ( 𝐹 ‘ 𝑧 ) ) )
32	10 30 31	sylanbrc	⊢ ( 𝑅 Or 𝑉 → 𝐹 : 𝑃 –onto→ 𝑂 )
33		df-f1o	⊢ ( 𝐹 : 𝑃 –1-1-onto→ 𝑂 ↔ ( 𝐹 : 𝑃 –1-1→ 𝑂 ∧ 𝐹 : 𝑃 –onto→ 𝑂 ) )
34	18 32 33	sylanbrc	⊢ ( 𝑅 Or 𝑉 → 𝐹 : 𝑃 –1-1-onto→ 𝑂 )