Theorem sprsymrelf1o

Description: The mapping F is a bijection between the subsets of the set of pairs over a fixed set V into the symmetric relations R on the fixed set V . (Contributed by AV, 23-Nov-2021)

	Ref	Expression
Hypotheses	sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
	sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
Assertion	sprsymrelf1o	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
4	1 2 3	sprsymrelf1	⊢ 𝐹 : 𝑃 –1-1→ 𝑅
5	4	a1i	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 –1-1→ 𝑅 )
6	1 2 3	sprsymrelfo	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 –onto→ 𝑅 )
7		df-f1o	⊢ ( 𝐹 : 𝑃 –1-1-onto→ 𝑅 ↔ ( 𝐹 : 𝑃 –1-1→ 𝑅 ∧ 𝐹 : 𝑃 –onto→ 𝑅 ) )
8	5 6 7	sylanbrc	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝑃 –1-1-onto→ 𝑅 )