Metamath Proof Explorer

Theorem subumgredg2

Description: An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020)

Ref Expression
Hypotheses subumgredg2.v ⊢ V = Vtx ⁡ S
subumgredg2.i ⊢ I = iEdg ⁡ S
Assertion subumgredg2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X ∈ e ∈ 𝒫 V | e = 2

Proof

Step Hyp Ref Expression
1 subumgredg2.v ⊢ V = Vtx ⁡ S
2 subumgredg2.i ⊢ I = iEdg ⁡ S
3 fveqeq2 ⊢ e = I ⁡ X → e = 2 ↔ I ⁡ X = 2
4 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
5 4 3ad2ant2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → G ∈ UHGraph
6 simp1 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → S SubGraph G
7 simp3 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → X ∈ dom ⁡ I
8 1 2 5 6 7 subgruhgredgd ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X ∈ 𝒫 V ∖ ∅
9 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
10 9 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
11 4 10 syl ⊢ G ∈ UMGraph → Fun ⁡ iEdg ⁡ G
12 11 3ad2ant2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → Fun ⁡ iEdg ⁡ G
13 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
14 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
15 eqid ⊢ Edg ⁡ S = Edg ⁡ S
16 13 14 2 9 15 subgrprop2 ⊢ S SubGraph G → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ I ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
17 16 simp2d ⊢ S SubGraph G → I ⊆ iEdg ⁡ G
18 17 3ad2ant1 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⊆ iEdg ⁡ G
19 funssfv ⊢ Fun ⁡ iEdg ⁡ G ∧ I ⊆ iEdg ⁡ G ∧ X ∈ dom ⁡ I → iEdg ⁡ G ⁡ X = I ⁡ X
20 19 eqcomd ⊢ Fun ⁡ iEdg ⁡ G ∧ I ⊆ iEdg ⁡ G ∧ X ∈ dom ⁡ I → I ⁡ X = iEdg ⁡ G ⁡ X
21 12 18 7 20 syl3anc ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X = iEdg ⁡ G ⁡ X
22 21 fveq2d ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X = iEdg ⁡ G ⁡ X
23 simp2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → G ∈ UMGraph
24 2 dmeqi ⊢ dom ⁡ I = dom ⁡ iEdg ⁡ S
25 24 eleq2i ⊢ X ∈ dom ⁡ I ↔ X ∈ dom ⁡ iEdg ⁡ S
26 subgreldmiedg ⊢ S SubGraph G ∧ X ∈ dom ⁡ iEdg ⁡ S → X ∈ dom ⁡ iEdg ⁡ G
27 26 ex ⊢ S SubGraph G → X ∈ dom ⁡ iEdg ⁡ S → X ∈ dom ⁡ iEdg ⁡ G
28 25 27 syl5bi ⊢ S SubGraph G → X ∈ dom ⁡ I → X ∈ dom ⁡ iEdg ⁡ G
29 28 a1d ⊢ S SubGraph G → G ∈ UMGraph → X ∈ dom ⁡ I → X ∈ dom ⁡ iEdg ⁡ G
30 29 3imp ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → X ∈ dom ⁡ iEdg ⁡ G
31 14 9 umgredg2 ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ X = 2
32 23 30 31 syl2anc ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → iEdg ⁡ G ⁡ X = 2
33 22 32 eqtrd ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X = 2
34 3 8 33 elrabd ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X ∈ e ∈ 𝒫 V ∖ ∅ | e = 2
35 prprrab ⊢ e ∈ 𝒫 V ∖ ∅ | e = 2 = e ∈ 𝒫 V | e = 2
36 34 35 eleqtrdi ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ X ∈ dom ⁡ I → I ⁡ X ∈ e ∈ 𝒫 V | e = 2