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 )