Theorem uspgrsprf1o

Description: The mapping F 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 . See also the comments on uspgrbisymrel . (Contributed by AV, 25-Nov-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3		uspgrsprf.f	⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
4	1 2 3	uspgrsprf1	⊢ 𝐹 : 𝐺 –1-1→ 𝑃
5	4	a1i	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 –1-1→ 𝑃 )
6	1 2 3	uspgrsprfo	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 –onto→ 𝑃 )
7		df-f1o	⊢ ( 𝐹 : 𝐺 –1-1-onto→ 𝑃 ↔ ( 𝐹 : 𝐺 –1-1→ 𝑃 ∧ 𝐹 : 𝐺 –onto→ 𝑃 ) )
8	5 6 7	sylanbrc	⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 –1-1-onto→ 𝑃 )