Theorem uspgrbisymrel

Description: There is a bijection between the "simple pseudographs" for a fixed set V of vertices and the class R of the symmetric relations on the fixed set V . The simple pseudographs, which are graphs without hyper- or multiedges, but which may contain loops, are expressed as ordered pairs of the vertices and the edges (as proper or improper unordered pairs of vertices, not as indexed edges!) in this theorem. That class G of such simple pseudographs is a set (if V is a set, see uspgrex ) of equivalence classes of graphs abstracting from the index sets of their edge functions.

Solely for this abstraction, there is a bijection between the "simple pseudographs" as members of G and the symmetric relations R on the fixed set V of vertices. This theorem would not hold for G = { g e. USPGraph | ( Vtxg ) = V } and even not for G = { <. v , e >. | ( v = V /\ <. v , e >. e. USPGraph ) } , because these are much bigger classes. (Proposed by Gerard Lang, 16-Nov-2021.) (Contributed by AV, 27-Nov-2021)

	Ref	Expression
Hypotheses	uspgrbisymrel.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
	uspgrbisymrel.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
Assertion	uspgrbisymrel	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		uspgrbisymrel.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
2		uspgrbisymrel.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3	1 2	uspgrymrelen	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅 )
4		bren	⊢ ( 𝐺 ≈ 𝑅 ↔ ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 )
5	3 4	sylib	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑅 )