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

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

Proof

Step Hyp Ref Expression
1 dfsn2 ⊢ { 𝐵 } = { 𝐵 , 𝐵 }
2 1 opeq2i ⊢ ⟨ 𝐴 , { 𝐵 } ⟩ = ⟨ 𝐴 , { 𝐵 , 𝐵 } ⟩
3 2 sneqi ⊢ { ⟨ 𝐴 , { 𝐵 } ⟩ } = { ⟨ 𝐴 , { 𝐵 , 𝐵 } ⟩ }
4 3 opeq2i ⊢ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 } ⟩ } ⟩ = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐵 } ⟩ } ⟩
5 3simpa ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) )
6 id ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝑉 )
7 6 ancri ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
8 7 3ad2ant3 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
9 uspgr1eop ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
10 5 8 9 syl2anc ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐵 } ⟩ } ⟩ ∈ USPGraph )
11 4 10 eqeltrid ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑉 ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 } ⟩ } ⟩ ∈ USPGraph )