Theorem uspgrspren

Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class P of subsets of the set of pairs over the fixed set V are equinumerous. (Contributed by AV, 27-Nov-2021)

	Ref	Expression
Hypotheses	uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
Assertion	uspgrspren	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3	1 2	uspgrbispr	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑃 )
4		bren	⊢ ( 𝐺 ≈ 𝑃 ↔ ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑃 )
5	3 4	sylibr	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑃 )