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 )