This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )