Metamath Proof Explorer

Theorem umgr2v2e

Description: A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g ⊢G=V0AB1AB
Assertion umgr2v2e ⊢V∈W∧A∈V∧B∈V∧A≠B→G∈UMGraph

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢G=V0AB1AB
2 c0ex ⊢0∈V
3 1ex ⊢1∈V
4 2 3 pm3.2i ⊢0∈V∧1∈V
5 prex ⊢AB∈V
6 5 5 pm3.2i ⊢AB∈V∧AB∈V
7 0ne1 ⊢0≠1
8 7 a1i ⊢V∈W∧A∈V∧B∈V∧A≠B→0≠1
9 fprg ⊢0∈V∧1∈V∧AB∈V∧AB∈V∧0≠1→0AB1AB:01⟶ABAB
10 4 6 8 9 mp3an12i ⊢V∈W∧A∈V∧B∈V∧A≠B→0AB1AB:01⟶ABAB
11 dfsn2 ⊢AB=ABAB
12 fveqeq2 ⊢e=AB→e=2↔AB=2
13 prelpwi ⊢A∈V∧B∈V→AB∈𝒫V
14 13 3adant1 ⊢V∈W∧A∈V∧B∈V→AB∈𝒫V
15 1 umgr2v2evtx ⊢V∈W→Vtx⁡G=V
16 15 3ad2ant1 ⊢V∈W∧A∈V∧B∈V→Vtx⁡G=V
17 16 pweqd ⊢V∈W∧A∈V∧B∈V→𝒫Vtx⁡G=𝒫V
18 14 17 eleqtrrd ⊢V∈W∧A∈V∧B∈V→AB∈𝒫Vtx⁡G
19 18 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B→AB∈𝒫Vtx⁡G
20 hashprg ⊢A∈V∧B∈V→A≠B↔AB=2
21 20 biimpd ⊢A∈V∧B∈V→A≠B→AB=2
22 21 3adant1 ⊢V∈W∧A∈V∧B∈V→A≠B→AB=2
23 22 imp ⊢V∈W∧A∈V∧B∈V∧A≠B→AB=2
24 12 19 23 elrabd ⊢V∈W∧A∈V∧B∈V∧A≠B→AB∈e∈𝒫Vtx⁡G|e=2
25 24 snssd ⊢V∈W∧A∈V∧B∈V∧A≠B→AB⊆e∈𝒫Vtx⁡G|e=2
26 11 25 eqsstrrid ⊢V∈W∧A∈V∧B∈V∧A≠B→ABAB⊆e∈𝒫Vtx⁡G|e=2
27 10 26 fssd ⊢V∈W∧A∈V∧B∈V∧A≠B→0AB1AB:01⟶e∈𝒫Vtx⁡G|e=2
28 27 ffdmd ⊢V∈W∧A∈V∧B∈V∧A≠B→0AB1AB:dom⁡0AB1AB⟶e∈𝒫Vtx⁡G|e=2
29 1 umgr2v2eiedg ⊢V∈W∧A∈V∧B∈V→iEdg⁡G=0AB1AB
30 29 adantr ⊢V∈W∧A∈V∧B∈V∧A≠B→iEdg⁡G=0AB1AB
31 30 dmeqd ⊢V∈W∧A∈V∧B∈V∧A≠B→dom⁡iEdg⁡G=dom⁡0AB1AB
32 30 31 feq12d ⊢V∈W∧A∈V∧B∈V∧A≠B→iEdg⁡G:dom⁡iEdg⁡G⟶e∈𝒫Vtx⁡G|e=2↔0AB1AB:dom⁡0AB1AB⟶e∈𝒫Vtx⁡G|e=2
33 28 32 mpbird ⊢V∈W∧A∈V∧B∈V∧A≠B→iEdg⁡G:dom⁡iEdg⁡G⟶e∈𝒫Vtx⁡G|e=2
34 opex ⊢V0AB1AB∈V
35 1 34 eqeltri ⊢G∈V
36 eqid ⊢Vtx⁡G=Vtx⁡G
37 eqid ⊢iEdg⁡G=iEdg⁡G
38 36 37 isumgrs ⊢G∈V→G∈UMGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶e∈𝒫Vtx⁡G|e=2
39 35 38 mp1i ⊢V∈W∧A∈V∧B∈V∧A≠B→G∈UMGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶e∈𝒫Vtx⁡G|e=2
40 33 39 mpbird ⊢V∈W∧A∈V∧B∈V∧A≠B→G∈UMGraph