Theorem uspgrbispr

Description: There is a bijection between the "simple pseudographs" with a fixed set of vertices V and the subsets of the set of pairs over the set V . (Contributed by AV, 26-Nov-2021)

	Ref	Expression
Hypotheses	uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
Assertion	uspgrbispr	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3	1 2	uspgrex	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ∈ V )
4	3	mptexd	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) ∈ V )
5		eqid	⊢ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
6	1 2 5	uspgrsprf1o	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) : 𝐺 –1-1-onto→ 𝑃 )
7		f1oeq1	⊢ ( 𝑓 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) → ( 𝑓 : 𝐺 –1-1-onto→ 𝑃 ↔ ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) ) : 𝐺 –1-1-onto→ 𝑃 ) )
8	4 6 7	spcedv	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑓 𝑓 : 𝐺 –1-1-onto→ 𝑃 )