Metamath Proof Explorer


Theorem usgredgsscusgredg

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 usgredgsscusgredg
|- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E C_ F )

Proof

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 usgredg
 |-  ( ( G e. USGraph /\ e e. E ) -> E. a e. V E. b e. V ( a =/= b /\ e = { a , b } ) )
6 3 4 iscusgredg
 |-  ( H e. ComplUSGraph <-> ( H e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. F ) )
7 sneq
 |-  ( k = a -> { k } = { a } )
8 7 difeq2d
 |-  ( k = a -> ( V \ { k } ) = ( V \ { a } ) )
9 preq2
 |-  ( k = a -> { n , k } = { n , a } )
10 9 eleq1d
 |-  ( k = a -> ( { n , k } e. F <-> { n , a } e. F ) )
11 8 10 raleqbidv
 |-  ( k = a -> ( A. n e. ( V \ { k } ) { n , k } e. F <-> A. n e. ( V \ { a } ) { n , a } e. F ) )
12 11 rspcv
 |-  ( a e. V -> ( A. k e. V A. n e. ( V \ { k } ) { n , k } e. F -> A. n e. ( V \ { a } ) { n , a } e. F ) )
13 simpl
 |-  ( ( a =/= b /\ e = { a , b } ) -> a =/= b )
14 13 necomd
 |-  ( ( a =/= b /\ e = { a , b } ) -> b =/= a )
15 14 anim2i
 |-  ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> ( b e. V /\ b =/= a ) )
16 eldifsn
 |-  ( b e. ( V \ { a } ) <-> ( b e. V /\ b =/= a ) )
17 15 16 sylibr
 |-  ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> b e. ( V \ { a } ) )
18 preq1
 |-  ( n = b -> { n , a } = { b , a } )
19 18 eleq1d
 |-  ( n = b -> ( { n , a } e. F <-> { b , a } e. F ) )
20 19 rspcv
 |-  ( b e. ( V \ { a } ) -> ( A. n e. ( V \ { a } ) { n , a } e. F -> { b , a } e. F ) )
21 17 20 syl
 |-  ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> ( A. n e. ( V \ { a } ) { n , a } e. F -> { b , a } e. F ) )
22 prcom
 |-  { a , b } = { b , a }
23 22 eqeq2i
 |-  ( e = { a , b } <-> e = { b , a } )
24 eqcom
 |-  ( e = { b , a } <-> { b , a } = e )
25 23 24 sylbb
 |-  ( e = { a , b } -> { b , a } = e )
26 25 eleq1d
 |-  ( e = { a , b } -> ( { b , a } e. F <-> e e. F ) )
27 26 biimpd
 |-  ( e = { a , b } -> ( { b , a } e. F -> e e. F ) )
28 27 ad2antll
 |-  ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> ( { b , a } e. F -> e e. F ) )
29 21 28 syld
 |-  ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> ( A. n e. ( V \ { a } ) { n , a } e. F -> e e. F ) )
30 12 29 syl9
 |-  ( a e. V -> ( ( b e. V /\ ( a =/= b /\ e = { a , b } ) ) -> ( A. k e. V A. n e. ( V \ { k } ) { n , k } e. F -> e e. F ) ) )
31 30 impl
 |-  ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ e = { a , b } ) ) -> ( A. k e. V A. n e. ( V \ { k } ) { n , k } e. F -> e e. F ) )
32 31 adantld
 |-  ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ e = { a , b } ) ) -> ( ( H e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. F ) -> e e. F ) )
33 6 32 syl5bi
 |-  ( ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ e = { a , b } ) ) -> ( H e. ComplUSGraph -> e e. F ) )
34 33 ex
 |-  ( ( a e. V /\ b e. V ) -> ( ( a =/= b /\ e = { a , b } ) -> ( H e. ComplUSGraph -> e e. F ) ) )
35 34 rexlimivv
 |-  ( E. a e. V E. b e. V ( a =/= b /\ e = { a , b } ) -> ( H e. ComplUSGraph -> e e. F ) )
36 5 35 syl
 |-  ( ( G e. USGraph /\ e e. E ) -> ( H e. ComplUSGraph -> e e. F ) )
37 36 impancom
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( e e. E -> e e. F ) )
38 37 ssrdv
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E C_ F )