Theorem griedg0ssusgr

Description: The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Hypothesis	griedg0prc.u	|- U = { <. v , e >. | e : (/) --> (/) }
Assertion	griedg0ssusgr	|- U C_ USGraph

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	|- U = { <. v , e >. | e : (/) --> (/) }
2	1	eleq2i	|- ( g e. U <-> g e. { <. v , e >. | e : (/) --> (/) } )
3		elopab	|- ( g e. { <. v , e >. | e : (/) --> (/) } <-> E. v E. e ( g = <. v , e >. /\ e : (/) --> (/) ) )
4	2 3	bitri	|- ( g e. U <-> E. v E. e ( g = <. v , e >. /\ e : (/) --> (/) ) )
5		opex	|- <. v , e >. e. _V
6	5	a1i	|- ( e : (/) --> (/) -> <. v , e >. e. _V )
7		vex	|- v e. _V
8		vex	|- e e. _V
9	7 8	opiedgfvi	|- ( iEdg ` <. v , e >. ) = e
10		f0bi	|- ( e : (/) --> (/) <-> e = (/) )
11	10	biimpi	|- ( e : (/) --> (/) -> e = (/) )
12	9 11	syl5eq	|- ( e : (/) --> (/) -> ( iEdg ` <. v , e >. ) = (/) )
13	6 12	usgr0e	|- ( e : (/) --> (/) -> <. v , e >. e. USGraph )
14	13	adantl	|- ( ( g = <. v , e >. /\ e : (/) --> (/) ) -> <. v , e >. e. USGraph )
15		eleq1	|- ( g = <. v , e >. -> ( g e. USGraph <-> <. v , e >. e. USGraph ) )
16	15	adantr	|- ( ( g = <. v , e >. /\ e : (/) --> (/) ) -> ( g e. USGraph <-> <. v , e >. e. USGraph ) )
17	14 16	mpbird	|- ( ( g = <. v , e >. /\ e : (/) --> (/) ) -> g e. USGraph )
18	17	exlimivv	|- ( E. v E. e ( g = <. v , e >. /\ e : (/) --> (/) ) -> g e. USGraph )
19	4 18	sylbi	|- ( g e. U -> g e. USGraph )
20	19	ssriv	|- U C_ USGraph