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 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )

Proof

Step Hyp Ref Expression
1 prex { 𝐴 , 𝐵 } ∈ V
2 s1val ( { 𝐴 , 𝐵 } ∈ V → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
3 1 2 mp1i ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ⟨“ { 𝐴 , 𝐵 } ”⟩ = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } )
4 3 opeq2d ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ )
5 simp1 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → 𝑉𝑊 )
6 c0ex 0 ∈ V
7 6 a1i ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → 0 ∈ V )
8 3simpc ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( 𝐴𝑉𝐵𝑉 ) )
9 uspgr1eop ( ( ( 𝑉𝑊 ∧ 0 ∈ V ) ∧ ( 𝐴𝑉𝐵𝑉 ) ) → ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
10 5 7 8 9 syl21anc ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
11 4 10 eqeltrd ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ⟨ 𝑉 , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )