Theorem uspgrex

Description: The class G of all "simple pseudographs" with a fixed set of vertices V is a set. (Contributed by AV, 26-Nov-2021)

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

Proof

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