Metamath Proof Explorer

Theorem usgr1e

Description: A simple graph with one edge (with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses uspgr1e.v ⊢ V = Vtx ⁡ G
uspgr1e.a ⊢ φ → A ∈ X
uspgr1e.b ⊢ φ → B ∈ V
uspgr1e.c ⊢ φ → C ∈ V
uspgr1e.e ⊢ φ → iEdg ⁡ G = A B C
usgr1e.e ⊢ φ → B ≠ C
Assertion usgr1e ⊢ φ → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 uspgr1e.v ⊢ V = Vtx ⁡ G
2 uspgr1e.a ⊢ φ → A ∈ X
3 uspgr1e.b ⊢ φ → B ∈ V
4 uspgr1e.c ⊢ φ → C ∈ V
5 uspgr1e.e ⊢ φ → iEdg ⁡ G = A B C
6 usgr1e.e ⊢ φ → B ≠ C
7 1 2 3 4 5 uspgr1e ⊢ φ → G ∈ USHGraph
8 hashprg ⊢ B ∈ V ∧ C ∈ V → B ≠ C ↔ B C = 2
9 3 4 8 syl2anc ⊢ φ → B ≠ C ↔ B C = 2
10 6 9 mpbid ⊢ φ → B C = 2
11 prex ⊢ B C ∈ V
12 fveqeq2 ⊢ x = B C → x = 2 ↔ B C = 2
13 11 12 ralsn ⊢ ∀ x ∈ B C x = 2 ↔ B C = 2
14 10 13 sylibr ⊢ φ → ∀ x ∈ B C x = 2
15 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
16 15 a1i ⊢ φ → Edg ⁡ G = ran ⁡ iEdg ⁡ G
17 5 rneqd ⊢ φ → ran ⁡ iEdg ⁡ G = ran ⁡ A B C
18 rnsnopg ⊢ A ∈ X → ran ⁡ A B C = B C
19 2 18 syl ⊢ φ → ran ⁡ A B C = B C
20 16 17 19 3eqtrd ⊢ φ → Edg ⁡ G = B C
21 20 raleqdv ⊢ φ → ∀ x ∈ Edg ⁡ G x = 2 ↔ ∀ x ∈ B C x = 2
22 14 21 mpbird ⊢ φ → ∀ x ∈ Edg ⁡ G x = 2
23 usgruspgrb ⊢ G ∈ USGraph ↔ G ∈ USHGraph ∧ ∀ x ∈ Edg ⁡ G x = 2
24 7 22 23 sylanbrc ⊢ φ → G ∈ USGraph