Metamath Proof Explorer

Theorem usgr1eop

Description: A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1eop ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → B ≠ C → V A B C ∈ USGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ V A B C = Vtx ⁡ V A B C
2 simpllr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → A ∈ X
3 simplrl ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → B ∈ V
4 simpl ⊢ V ∈ W ∧ A ∈ X → V ∈ W
5 4 adantr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V ∈ W
6 snex ⊢ A B C ∈ V
7 6 a1i ⊢ B ≠ C → A B C ∈ V
8 opvtxfv ⊢ V ∈ W ∧ A B C ∈ V → Vtx ⁡ V A B C = V
9 5 7 8 syl2an ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → Vtx ⁡ V A B C = V
10 3 9 eleqtrrd ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → B ∈ Vtx ⁡ V A B C
11 simprr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → C ∈ V
12 6 a1i ⊢ B ∈ V ∧ C ∈ V → A B C ∈ V
13 4 12 8 syl2an ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → Vtx ⁡ V A B C = V
14 11 13 eleqtrrd ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → C ∈ Vtx ⁡ V A B C
15 14 adantr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → C ∈ Vtx ⁡ V A B C
16 opiedgfv ⊢ V ∈ W ∧ A B C ∈ V → iEdg ⁡ V A B C = A B C
17 5 7 16 syl2an ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → iEdg ⁡ V A B C = A B C
18 simpr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → B ≠ C
19 1 2 10 15 17 18 usgr1e ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ B ≠ C → V A B C ∈ USGraph
20 19 ex ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → B ≠ C → V A B C ∈ USGraph