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	|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , <" { A , B } "> >. e. USPGraph )

Proof

Step	Hyp	Ref	Expression
1		prex	|- { A , B } e. _V
2		s1val	|- ( { A , B } e. _V -> <" { A , B } "> = { <. 0 , { A , B } >. } )
3	1 2	mp1i	|- ( ( V e. W /\ A e. V /\ B e. V ) -> <" { A , B } "> = { <. 0 , { A , B } >. } )
4	3	opeq2d	|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , <" { A , B } "> >. = <. V , { <. 0 , { A , B } >. } >. )
5		simp1	|- ( ( V e. W /\ A e. V /\ B e. V ) -> V e. W )
6		c0ex	|- 0 e. _V
7	6	a1i	|- ( ( V e. W /\ A e. V /\ B e. V ) -> 0 e. _V )
8		3simpc	|- ( ( V e. W /\ A e. V /\ B e. V ) -> ( A e. V /\ B e. V ) )
9		uspgr1eop	|- ( ( ( V e. W /\ 0 e. _V ) /\ ( A e. V /\ B e. V ) ) -> <. V , { <. 0 , { A , B } >. } >. e. USPGraph )
10	5 7 8 9	syl21anc	|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , { <. 0 , { A , B } >. } >. e. USPGraph )
11	4 10	eqeltrd	|- ( ( V e. W /\ A e. V /\ B e. V ) -> <. V , <" { A , B } "> >. e. USPGraph )