Metamath Proof Explorer

Theorem uspgr1eop

Description: A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion uspgr1eop ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V A B C ∈ USHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ V A B C = Vtx ⁡ V A B C
2 simplr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → A ∈ X
3 simprl ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → B ∈ V
4 simpl ⊢ V ∈ W ∧ A ∈ X → V ∈ W
5 snex ⊢ A B C ∈ V
6 5 a1i ⊢ B ∈ V ∧ C ∈ V → A B C ∈ V
7 opvtxfv ⊢ V ∈ W ∧ A B C ∈ V → Vtx ⁡ V A B C = V
8 4 6 7 syl2an ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → Vtx ⁡ V A B C = V
9 3 8 eleqtrrd ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → B ∈ Vtx ⁡ V A B C
10 simprr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → C ∈ V
11 10 8 eleqtrrd ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → C ∈ Vtx ⁡ V A B C
12 opiedgfv ⊢ V ∈ W ∧ A B C ∈ V → iEdg ⁡ V A B C = A B C
13 4 6 12 syl2an ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → iEdg ⁡ V A B C = A B C
14 1 2 9 11 13 uspgr1e ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V A B C ∈ USHGraph