Metamath Proof Explorer

Theorem uspgr1v1eop

Description: A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 dfsn2 ⊢ B = B B
2 1 opeq2i ⊢ A B = A B B
3 2 sneqi ⊢ A B = A B B
4 3 opeq2i ⊢ V A B = V A B B
5 3simpa ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V → V ∈ W ∧ A ∈ X
6 id ⊢ B ∈ V → B ∈ V
7 6 ancri ⊢ B ∈ V → B ∈ V ∧ B ∈ V
8 7 3ad2ant3 ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V → B ∈ V ∧ B ∈ V
9 uspgr1eop ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ B ∈ V → V A B B ∈ USHGraph
10 5 8 9 syl2anc ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V → V A B B ∈ USHGraph
11 4 10 eqeltrid ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V → V A B ∈ USHGraph