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 = v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ 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 = v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ 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 ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → V ∈ W ↔ v ∈ W
6 5 biimpac ⊢ V ∈ W ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ 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 ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → v = V → e ∈ P
26 25 impcom ⊢ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ∈ P
27 26 adantl ⊢ V ∈ W ∧ v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e → e ∈ P
28 6 27 opabssxpd ⊢ V ∈ W → v e | v = V ∧ ∃ q ∈ USHGraph Vtx ⁡ q = v ∧ Edg ⁡ q = e ⊆ W × P
29 2 28 eqsstrid ⊢ V ∈ W → G ⊆ W × P