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	$$⊢\left(V\in W\wedge A\in X\wedge B\in V\right)\to ⟨V,\left\{⟨A,\left\{B\right\}⟩\right\}⟩\in \mathrm{USHGraph}$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{B\right\}=\left\{B,B\right\}$$
2	1	opeq2i	$$⊢⟨A,\left\{B\right\}⟩=⟨A,\left\{B,B\right\}⟩$$
3	2	sneqi	$$⊢\left\{⟨A,\left\{B\right\}⟩\right\}=\left\{⟨A,\left\{B,B\right\}⟩\right\}$$
4	3	opeq2i	$$⊢⟨V,\left\{⟨A,\left\{B\right\}⟩\right\}⟩=⟨V,\left\{⟨A,\left\{B,B\right\}⟩\right\}⟩$$
5		3simpa	$$⊢\left(V\in W\wedge A\in X\wedge B\in V\right)\to \left(V\in W\wedge A\in X\right)$$
6		id	$$⊢B\in V\to B\in V$$
7	6	ancri	$$⊢B\in V\to \left(B\in V\wedge B\in V\right)$$
8	7	3ad2ant3	$$⊢\left(V\in W\wedge A\in X\wedge B\in V\right)\to \left(B\in V\wedge B\in V\right)$$
9		uspgr1eop	$$⊢\left(\left(V\in W\wedge A\in X\right)\wedge \left(B\in V\wedge B\in V\right)\right)\to ⟨V,\left\{⟨A,\left\{B,B\right\}⟩\right\}⟩\in \mathrm{USHGraph}$$
10	5 8 9	syl2anc	$$⊢\left(V\in W\wedge A\in X\wedge B\in V\right)\to ⟨V,\left\{⟨A,\left\{B,B\right\}⟩\right\}⟩\in \mathrm{USHGraph}$$
11	4 10	eqeltrid	$$⊢\left(V\in W\wedge A\in X\wedge B\in V\right)\to ⟨V,\left\{⟨A,\left\{B\right\}⟩\right\}⟩\in \mathrm{USHGraph}$$