Theorem upgr1eop

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 10-Oct-2020)

	Ref	Expression
Assertion	upgr1eop	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = ( Vtx ` <. V , { <. A , { B , C } >. } >. )
2		simplr	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> A e. X )
3		simprl	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> B e. V )
4		simpl	|- ( ( V e. W /\ A e. X ) -> V e. W )
5		snex	|- { <. A , { B , C } >. } e. _V
6	5	a1i	|- ( ( B e. V /\ C e. V ) -> { <. A , { B , C } >. } e. _V )
7		opvtxfv	|- ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
8	4 6 7	syl2an	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V )
9	3 8	eleqtrrd	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> B e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
10		simprr	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. V )
11	10 8	eleqtrrd	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) )
12		opiedgfv	|- ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
13	4 6 12	syl2an	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } )
14	1 2 9 11 13	upgr1e	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. UPGraph )