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 )