Metamath Proof Explorer

Theorem uspgr1ewop

Description: A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021)

Ref Expression
Assertion uspgr1ewop ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → V ⟨“ A B ”⟩ ∈ USHGraph

Proof

Step Hyp Ref Expression
1 prex ⊢ A B ∈ V
2 s1val ⊢ A B ∈ V → ⟨“ A B ”⟩ = 0 A B
3 1 2 mp1i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → ⟨“ A B ”⟩ = 0 A B
4 3 opeq2d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → V ⟨“ A B ”⟩ = V 0 A B
5 simp1 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → V ∈ W
6 c0ex ⊢ 0 ∈ V
7 6 a1i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → 0 ∈ V
8 3simpc ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A ∈ V ∧ B ∈ V
9 uspgr1eop ⊢ V ∈ W ∧ 0 ∈ V ∧ A ∈ V ∧ B ∈ V → V 0 A B ∈ USHGraph
10 5 7 8 9 syl21anc ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → V 0 A B ∈ USHGraph
11 4 10 eqeltrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → V ⟨“ A B ”⟩ ∈ USHGraph