Theorem uspgrsprfv

Description: The value of the function F which maps a "simple pseudograph" for a fixed set V of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for G as defined here, the function F is a bijection between the "simple pseudographs" and the subsets of the set of pairs P over the fixed set V of vertices, see uspgrbispr . (Contributed by AV, 24-Nov-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3		uspgrsprf.f	⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
4		fveq2	⊢ ( 𝑔 = 𝑋 → ( 2nd ‘ 𝑔 ) = ( 2nd ‘ 𝑋 ) )
5		id	⊢ ( 𝑋 ∈ 𝐺 → 𝑋 ∈ 𝐺 )
6		fvexd	⊢ ( 𝑋 ∈ 𝐺 → ( 2nd ‘ 𝑋 ) ∈ V )
7	3 4 5 6	fvmptd3	⊢ ( 𝑋 ∈ 𝐺 → ( 𝐹 ‘ 𝑋 ) = ( 2nd ‘ 𝑋 ) )