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→VABC∈USGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡VABC=Vtx⁡VABC
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 ⊢ABC∈V
7 6 a1i ⊢B≠C→ABC∈V
8 opvtxfv ⊢V∈W∧ABC∈V→Vtx⁡VABC=V
9 5 7 8 syl2an ⊢V∈W∧A∈X∧B∈V∧C∈V∧B≠C→Vtx⁡VABC=V
10 3 9 eleqtrrd ⊢V∈W∧A∈X∧B∈V∧C∈V∧B≠C→B∈Vtx⁡VABC
11 simprr ⊢V∈W∧A∈X∧B∈V∧C∈V→C∈V
12 6 a1i ⊢B∈V∧C∈V→ABC∈V
13 4 12 8 syl2an ⊢V∈W∧A∈X∧B∈V∧C∈V→Vtx⁡VABC=V
14 11 13 eleqtrrd ⊢V∈W∧A∈X∧B∈V∧C∈V→C∈Vtx⁡VABC
15 14 adantr ⊢V∈W∧A∈X∧B∈V∧C∈V∧B≠C→C∈Vtx⁡VABC
16 opiedgfv ⊢V∈W∧ABC∈V→iEdg⁡VABC=ABC
17 5 7 16 syl2an ⊢V∈W∧A∈X∧B∈V∧C∈V∧B≠C→iEdg⁡VABC=ABC
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→VABC∈USGraph
20 19 ex ⊢V∈W∧A∈X∧B∈V∧C∈V→B≠C→VABC∈USGraph