Description: A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 13-Nov-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fusgrmaxsize.v | |- V = ( Vtx ` G ) |
|
| fusgrmaxsize.e | |- E = ( Edg ` G ) |
||
| usgrsscusgra.h | |- V = ( Vtx ` H ) |
||
| usgrsscusgra.f | |- F = ( Edg ` H ) |
||
| Assertion | usgrsscusgr | |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> A. e e. E E. f e. F e = f ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fusgrmaxsize.v | |- V = ( Vtx ` G ) |
|
| 2 | fusgrmaxsize.e | |- E = ( Edg ` G ) |
|
| 3 | usgrsscusgra.h | |- V = ( Vtx ` H ) |
|
| 4 | usgrsscusgra.f | |- F = ( Edg ` H ) |
|
| 5 | 1 2 3 4 | usgredgsscusgredg | |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E C_ F ) |
| 6 | dfss5 | |- ( E C_ F <-> A. e e. E E. f e. F e = f ) |
|
| 7 | 5 6 | sylib | |- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> A. e e. E E. f e. F e = f ) |