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 ) |