Metamath Proof Explorer


Theorem uspgrymrelen

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class R of the symmetric relations on the fixed set V are equinumerous. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 27-Nov-2021)

Ref Expression
Hypotheses uspgrbisymrel.g 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
uspgrbisymrel.r 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥𝑉𝑦𝑉 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) }
Assertion uspgrymrelen ( 𝑉𝑊𝐺𝑅 )

Proof

Step Hyp Ref Expression
1 uspgrbisymrel.g 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
2 uspgrbisymrel.r 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥𝑉𝑦𝑉 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) }
3 eqid 𝒫 ( Pairs ‘ 𝑉 ) = 𝒫 ( Pairs ‘ 𝑉 )
4 3 1 uspgrspren ( 𝑉𝑊𝐺 ≈ 𝒫 ( Pairs ‘ 𝑉 ) )
5 3 2 sprsymrelen ( 𝑉𝑊 → 𝒫 ( Pairs ‘ 𝑉 ) ≈ 𝑅 )
6 entr ( ( 𝐺 ≈ 𝒫 ( Pairs ‘ 𝑉 ) ∧ 𝒫 ( Pairs ‘ 𝑉 ) ≈ 𝑅 ) → 𝐺𝑅 )
7 4 5 6 syl2anc ( 𝑉𝑊𝐺𝑅 )