Metamath Proof Explorer

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 ⊢P=𝒫Pairs⁡V
uspgrsprf.g ⊢G=ve|v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e
Assertion uspgropssxp ⊢V∈W→G⊆W×P

Proof

Step Hyp Ref Expression
1 uspgrsprf.p ⊢P=𝒫Pairs⁡V
2 uspgrsprf.g ⊢G=ve|v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e
3 eleq1 ⊢V=v→V∈W↔v∈W
4 3 eqcoms ⊢v=V→V∈W↔v∈W
5 4 adantr ⊢v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e→V∈W↔v∈W
6 5 biimpac ⊢V∈W∧v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e→v∈W
7 uspgrupgr ⊢q∈USHGraph→q∈UPGraph
8 upgredgssspr ⊢q∈UPGraph→Edg⁡q⊆Pairs⁡Vtx⁡q
9 7 8 syl ⊢q∈USHGraph→Edg⁡q⊆Pairs⁡Vtx⁡q
10 9 3ad2ant1 ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Edg⁡q⊆Pairs⁡Vtx⁡q
11 simp2l ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Vtx⁡q=v
12 simp3 ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→v=V
13 11 12 eqtrd ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Vtx⁡q=V
14 13 fveq2d ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Pairs⁡Vtx⁡q=Pairs⁡V
15 10 14 sseqtrd ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Edg⁡q⊆Pairs⁡V
16 fvex ⊢Edg⁡q∈V
17 16 elpw ⊢Edg⁡q∈𝒫Pairs⁡V↔Edg⁡q⊆Pairs⁡V
18 15 17 sylibr ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→Edg⁡q∈𝒫Pairs⁡V
19 simpr ⊢Vtx⁡q=v∧Edg⁡q=e→Edg⁡q=e
20 19 eqcomd ⊢Vtx⁡q=v∧Edg⁡q=e→e=Edg⁡q
21 20 3ad2ant2 ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→e=Edg⁡q
22 1 a1i ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→P=𝒫Pairs⁡V
23 18 21 22 3eltr4d ⊢q∈USHGraph∧Vtx⁡q=v∧Edg⁡q=e∧v=V→e∈P
24 23 3exp ⊢q∈USHGraph→Vtx⁡q=v∧Edg⁡q=e→v=V→e∈P
25 24 rexlimiv ⊢∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e→v=V→e∈P
26 25 impcom ⊢v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e→e∈P
27 26 adantl ⊢V∈W∧v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e→e∈P
28 6 27 opabssxpd ⊢V∈W→ve|v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e⊆W×P
29 2 28 eqsstrid ⊢V∈W→G⊆W×P