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 = V 0 A B 1 A B
Assertion umgr2v2e ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → G ∈ UMGraph

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
2 c0ex ⊢ 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 2 3 pm3.2i ⊢ 0 ∈ V ∧ 1 ∈ V
5 prex ⊢ A B ∈ V
6 5 5 pm3.2i ⊢ A B ∈ V ∧ A B ∈ V
7 0ne1 ⊢ 0 ≠ 1
8 7 a1i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → 0 ≠ 1
9 fprg ⊢ 0 ∈ V ∧ 1 ∈ V ∧ A B ∈ V ∧ A B ∈ V ∧ 0 ≠ 1 → 0 A B 1 A B : 0 1 ⟶ A B A B
10 4 6 8 9 mp3an12i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → 0 A B 1 A B : 0 1 ⟶ A B A B
11 dfsn2 ⊢ A B = A B A B
12 fveqeq2 ⊢ e = A B → e = 2 ↔ A B = 2
13 prelpwi ⊢ A ∈ V ∧ B ∈ V → A B ∈ 𝒫 V
14 13 3adant1 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A B ∈ 𝒫 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 → A B ∈ 𝒫 Vtx ⁡ G
19 18 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B ∈ 𝒫 Vtx ⁡ G
20 hashprg ⊢ A ∈ V ∧ B ∈ V → A ≠ B ↔ A B = 2
21 20 biimpd ⊢ A ∈ V ∧ B ∈ V → A ≠ B → A B = 2
22 21 3adant1 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A ≠ B → A B = 2
23 22 imp ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B = 2
24 12 19 23 elrabd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B ∈ e ∈ 𝒫 Vtx ⁡ G | e = 2
25 24 snssd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B ⊆ e ∈ 𝒫 Vtx ⁡ G | e = 2
26 11 25 eqsstrrid ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B A B ⊆ e ∈ 𝒫 Vtx ⁡ G | e = 2
27 10 26 fssd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → 0 A B 1 A B : 0 1 ⟶ e ∈ 𝒫 Vtx ⁡ G | e = 2
28 27 ffdmd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → 0 A B 1 A B : dom ⁡ 0 A B 1 A B ⟶ e ∈ 𝒫 Vtx ⁡ G | e = 2
29 1 umgr2v2eiedg ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → iEdg ⁡ G = 0 A B 1 A B
30 29 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → iEdg ⁡ G = 0 A B 1 A B
31 30 dmeqd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → dom ⁡ iEdg ⁡ G = dom ⁡ 0 A B 1 A B
32 30 31 feq12d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ e ∈ 𝒫 Vtx ⁡ G | e = 2 ↔ 0 A B 1 A B : dom ⁡ 0 A B 1 A B ⟶ 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 ⊢ V 0 A B 1 A B ∈ 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