This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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