Theorem sprbisymrel

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

	Ref	Expression
Hypotheses	sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
Assertion	sprbisymrel	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		fvex	⊢ ( Pairs ‘ 𝑉 ) ∈ V
4	3	pwex	⊢ 𝒫 ( Pairs ‘ 𝑉 ) ∈ V
5	1 4	eqeltri	⊢ 𝑃 ∈ V
6		mptexg	⊢ ( 𝑃 ∈ V → ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V )
7	5 6	mp1i	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V )
8		eqid	⊢ ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
9	1 2 8	sprsymrelf1o	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) : 𝑃 –1-1-onto→ 𝑅 )
10		f1oeq1	⊢ ( 𝑓 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) → ( 𝑓 : 𝑃 –1-1-onto→ 𝑅 ↔ ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) : 𝑃 –1-1-onto→ 𝑅 ) )
11	10	spcegv	⊢ ( ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) ∈ V → ( ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } ) : 𝑃 –1-1-onto→ 𝑅 → ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑅 ) )
12	7 9 11	sylc	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝑃 –1-1-onto→ 𝑅 )