Metamath Proof Explorer

Theorem upgr1eop

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgr1eop ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V A B C ∈ UPGraph

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 upgr1e ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V A B C ∈ UPGraph