Metamath Proof Explorer


Theorem isumgr

Description: The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v V=VtxG
isumgr.e E=iEdgG
Assertion isumgr GUGUMGraphE:domEx𝒫V|x=2

Proof

Step Hyp Ref Expression
1 isumgr.v V=VtxG
2 isumgr.e E=iEdgG
3 df-umgr UMGraph=g|[˙Vtxg/v]˙[˙iEdgg/e]˙e:domex𝒫v|x=2
4 3 eleq2i GUMGraphGg|[˙Vtxg/v]˙[˙iEdgg/e]˙e:domex𝒫v|x=2
5 fveq2 h=GiEdgh=iEdgG
6 5 2 eqtr4di h=GiEdgh=E
7 5 dmeqd h=GdomiEdgh=domiEdgG
8 2 eqcomi iEdgG=E
9 8 dmeqi domiEdgG=domE
10 7 9 eqtrdi h=GdomiEdgh=domE
11 fveq2 h=GVtxh=VtxG
12 11 1 eqtr4di h=GVtxh=V
13 12 pweqd h=G𝒫Vtxh=𝒫V
14 13 difeq1d h=G𝒫Vtxh=𝒫V
15 14 rabeqdv h=Gx𝒫Vtxh|x=2=x𝒫V|x=2
16 6 10 15 feq123d h=GiEdgh:domiEdghx𝒫Vtxh|x=2E:domEx𝒫V|x=2
17 fvexd g=hVtxgV
18 fveq2 g=hVtxg=Vtxh
19 fvexd g=hv=VtxhiEdggV
20 fveq2 g=hiEdgg=iEdgh
21 20 adantr g=hv=VtxhiEdgg=iEdgh
22 simpr g=hv=Vtxhe=iEdghe=iEdgh
23 22 dmeqd g=hv=Vtxhe=iEdghdome=domiEdgh
24 pweq v=Vtxh𝒫v=𝒫Vtxh
25 24 ad2antlr g=hv=Vtxhe=iEdgh𝒫v=𝒫Vtxh
26 25 difeq1d g=hv=Vtxhe=iEdgh𝒫v=𝒫Vtxh
27 26 rabeqdv g=hv=Vtxhe=iEdghx𝒫v|x=2=x𝒫Vtxh|x=2
28 22 23 27 feq123d g=hv=Vtxhe=iEdghe:domex𝒫v|x=2iEdgh:domiEdghx𝒫Vtxh|x=2
29 19 21 28 sbcied2 g=hv=Vtxh[˙iEdgg/e]˙e:domex𝒫v|x=2iEdgh:domiEdghx𝒫Vtxh|x=2
30 17 18 29 sbcied2 g=h[˙Vtxg/v]˙[˙iEdgg/e]˙e:domex𝒫v|x=2iEdgh:domiEdghx𝒫Vtxh|x=2
31 30 cbvabv g|[˙Vtxg/v]˙[˙iEdgg/e]˙e:domex𝒫v|x=2=h|iEdgh:domiEdghx𝒫Vtxh|x=2
32 16 31 elab2g GUGg|[˙Vtxg/v]˙[˙iEdgg/e]˙e:domex𝒫v|x=2E:domEx𝒫V|x=2
33 4 32 syl5bb GUGUMGraphE:domEx𝒫V|x=2