Theorem uspgropssxp

Description: The set G of "simple pseudographs" for a fixed set V of vertices is a subset of a Cartesian product. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 24-Nov-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uspgrsprf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		uspgrsprf.g	⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3		eleq1	⊢ ( 𝑉 = 𝑣 → ( 𝑉 ∈ 𝑊 ↔ 𝑣 ∈ 𝑊 ) )
4	3	eqcoms	⊢ ( 𝑣 = 𝑉 → ( 𝑉 ∈ 𝑊 ↔ 𝑣 ∈ 𝑊 ) )
5	4	adantr	⊢ ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → ( 𝑉 ∈ 𝑊 ↔ 𝑣 ∈ 𝑊 ) )
6	5	biimpac	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → 𝑣 ∈ 𝑊 )
7		uspgrupgr	⊢ ( 𝑞 ∈ USPGraph → 𝑞 ∈ UPGraph )
8		upgredgssspr	⊢ ( 𝑞 ∈ UPGraph → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
9	7 8	syl	⊢ ( 𝑞 ∈ USPGraph → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
10	9	3ad2ant1	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) )
11		simp2l	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Vtx ‘ 𝑞 ) = 𝑣 )
12		simp3	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
13	11 12	eqtrd	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Vtx ‘ 𝑞 ) = 𝑉 )
14	13	fveq2d	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Pairs ‘ ( Vtx ‘ 𝑞 ) ) = ( Pairs ‘ 𝑉 ) )
15	10 14	sseqtrd	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ 𝑉 ) )
16		fvex	⊢ ( Edg ‘ 𝑞 ) ∈ V
17	16	elpw	⊢ ( ( Edg ‘ 𝑞 ) ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ ( Edg ‘ 𝑞 ) ⊆ ( Pairs ‘ 𝑉 ) )
18	15 17	sylibr	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → ( Edg ‘ 𝑞 ) ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
19		simpr	⊢ ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( Edg ‘ 𝑞 ) = 𝑒 )
20	19	eqcomd	⊢ ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → 𝑒 = ( Edg ‘ 𝑞 ) )
21	20	3ad2ant2	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → 𝑒 = ( Edg ‘ 𝑞 ) )
22	1	a1i	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → 𝑃 = 𝒫 ( Pairs ‘ 𝑉 ) )
23	18 21 22	3eltr4d	⊢ ( ( 𝑞 ∈ USPGraph ∧ ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ∧ 𝑣 = 𝑉 ) → 𝑒 ∈ 𝑃 )
24	23	3exp	⊢ ( 𝑞 ∈ USPGraph → ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( 𝑣 = 𝑉 → 𝑒 ∈ 𝑃 ) ) )
25	24	rexlimiv	⊢ ( ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) → ( 𝑣 = 𝑉 → 𝑒 ∈ 𝑃 ) )
26	25	impcom	⊢ ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) → 𝑒 ∈ 𝑃 )
27	26	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → 𝑒 ∈ 𝑃 )
28	6 27	opabssxpd	⊢ ( 𝑉 ∈ 𝑊 → { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ⊆ ( 𝑊 × 𝑃 ) )
29	2 28	eqsstrid	⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ⊆ ( 𝑊 × 𝑃 ) )