Step |
Hyp |
Ref |
Expression |
1 |
|
snstrvtxval.v |
|- V e. _V |
2 |
|
snstrvtxval.g |
|- G = { <. ( Base ` ndx ) , V >. } |
3 |
|
iedgval |
|- ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) |
4 |
3
|
a1i |
|- ( V =/= ( Base ` ndx ) -> ( iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) ) |
5 |
|
necom |
|- ( V =/= ( Base ` ndx ) <-> ( Base ` ndx ) =/= V ) |
6 |
|
fvex |
|- ( Base ` ndx ) e. _V |
7 |
6 1 2
|
funsndifnop |
|- ( ( Base ` ndx ) =/= V -> -. G e. ( _V X. _V ) ) |
8 |
5 7
|
sylbi |
|- ( V =/= ( Base ` ndx ) -> -. G e. ( _V X. _V ) ) |
9 |
8
|
iffalsed |
|- ( V =/= ( Base ` ndx ) -> if ( G e. ( _V X. _V ) , ( 2nd ` G ) , ( .ef ` G ) ) = ( .ef ` G ) ) |
10 |
|
snex |
|- { <. ( Base ` ndx ) , V >. } e. _V |
11 |
10
|
a1i |
|- ( G = { <. ( Base ` ndx ) , V >. } -> { <. ( Base ` ndx ) , V >. } e. _V ) |
12 |
2 11
|
eqeltrid |
|- ( G = { <. ( Base ` ndx ) , V >. } -> G e. _V ) |
13 |
|
edgfndxid |
|- ( G e. _V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) ) |
14 |
2 12 13
|
mp2b |
|- ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) |
15 |
|
slotsbaseefdif |
|- ( Base ` ndx ) =/= ( .ef ` ndx ) |
16 |
15
|
nesymi |
|- -. ( .ef ` ndx ) = ( Base ` ndx ) |
17 |
16
|
a1i |
|- ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) = ( Base ` ndx ) ) |
18 |
|
fvex |
|- ( .ef ` ndx ) e. _V |
19 |
18
|
elsn |
|- ( ( .ef ` ndx ) e. { ( Base ` ndx ) } <-> ( .ef ` ndx ) = ( Base ` ndx ) ) |
20 |
17 19
|
sylnibr |
|- ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) e. { ( Base ` ndx ) } ) |
21 |
2
|
dmeqi |
|- dom G = dom { <. ( Base ` ndx ) , V >. } |
22 |
|
dmsnopg |
|- ( V e. _V -> dom { <. ( Base ` ndx ) , V >. } = { ( Base ` ndx ) } ) |
23 |
1 22
|
mp1i |
|- ( V =/= ( Base ` ndx ) -> dom { <. ( Base ` ndx ) , V >. } = { ( Base ` ndx ) } ) |
24 |
21 23
|
syl5eq |
|- ( V =/= ( Base ` ndx ) -> dom G = { ( Base ` ndx ) } ) |
25 |
20 24
|
neleqtrrd |
|- ( V =/= ( Base ` ndx ) -> -. ( .ef ` ndx ) e. dom G ) |
26 |
|
ndmfv |
|- ( -. ( .ef ` ndx ) e. dom G -> ( G ` ( .ef ` ndx ) ) = (/) ) |
27 |
25 26
|
syl |
|- ( V =/= ( Base ` ndx ) -> ( G ` ( .ef ` ndx ) ) = (/) ) |
28 |
14 27
|
syl5eq |
|- ( V =/= ( Base ` ndx ) -> ( .ef ` G ) = (/) ) |
29 |
4 9 28
|
3eqtrd |
|- ( V =/= ( Base ` ndx ) -> ( iEdg ` G ) = (/) ) |