Metamath Proof Explorer

Theorem umgrpredgv

Description: An edge of a multigraph always connects two vertices. Analogue of umgredgprv . This theorem does not hold for arbitrary pseudographs: if either M or N is a proper class, then { M , N } e. E could still hold ( { M , N } would be either { M } or { N } , see prprc1 or prprc2 , i.e. a loop), but M e. V or N e. V would not be true. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgredg.v ⊢ V = Vtx ⁡ G
upgredg.e ⊢ E = Edg ⁡ G
Assertion umgrpredgv ⊢ G ∈ UMGraph ∧ M N ∈ E → M ∈ V ∧ N ∈ V

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ V = Vtx ⁡ G
2 upgredg.e ⊢ E = Edg ⁡ G
3 2 eleq2i ⊢ M N ∈ E ↔ M N ∈ Edg ⁡ G
4 edgumgr ⊢ G ∈ UMGraph ∧ M N ∈ Edg ⁡ G → M N ∈ 𝒫 Vtx ⁡ G ∧ M N = 2
5 3 4 sylan2b ⊢ G ∈ UMGraph ∧ M N ∈ E → M N ∈ 𝒫 Vtx ⁡ G ∧ M N = 2
6 eqid ⊢ M N = M N
7 6 hashprdifel ⊢ M N = 2 → M ∈ M N ∧ N ∈ M N ∧ M ≠ N
8 1 eqcomi ⊢ Vtx ⁡ G = V
9 8 pweqi ⊢ 𝒫 Vtx ⁡ G = 𝒫 V
10 9 eleq2i ⊢ M N ∈ 𝒫 Vtx ⁡ G ↔ M N ∈ 𝒫 V
11 prelpw ⊢ M ∈ M N ∧ N ∈ M N → M ∈ V ∧ N ∈ V ↔ M N ∈ 𝒫 V
12 11 biimprd ⊢ M ∈ M N ∧ N ∈ M N → M N ∈ 𝒫 V → M ∈ V ∧ N ∈ V
13 10 12 syl5bi ⊢ M ∈ M N ∧ N ∈ M N → M N ∈ 𝒫 Vtx ⁡ G → M ∈ V ∧ N ∈ V
14 13 3adant3 ⊢ M ∈ M N ∧ N ∈ M N ∧ M ≠ N → M N ∈ 𝒫 Vtx ⁡ G → M ∈ V ∧ N ∈ V
15 7 14 syl ⊢ M N = 2 → M N ∈ 𝒫 Vtx ⁡ G → M ∈ V ∧ N ∈ V
16 15 impcom ⊢ M N ∈ 𝒫 Vtx ⁡ G ∧ M N = 2 → M ∈ V ∧ N ∈ V
17 5 16 syl ⊢ G ∈ UMGraph ∧ M N ∈ E → M ∈ V ∧ N ∈ V