| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isubgr3stgr.v |
|- V = ( Vtx ` G ) |
| 2 |
|
isubgr3stgr.u |
|- U = ( G NeighbVtx X ) |
| 3 |
|
isubgr3stgr.c |
|- C = ( G ClNeighbVtx X ) |
| 4 |
|
isubgr3stgr.n |
|- N e. NN0 |
| 5 |
|
isubgr3stgr.s |
|- S = ( StarGr ` N ) |
| 6 |
|
isubgr3stgr.w |
|- W = ( Vtx ` S ) |
| 7 |
|
isubgr3stgr.e |
|- E = ( Edg ` G ) |
| 8 |
|
preq2 |
|- ( z = ( F ` B ) -> { 0 , z } = { 0 , ( F ` B ) } ) |
| 9 |
8
|
eqeq2d |
|- ( z = ( F ` B ) -> ( ( F " { X , B } ) = { 0 , z } <-> ( F " { X , B } ) = { 0 , ( F ` B ) } ) ) |
| 10 |
|
f1of |
|- ( F : C -1-1-onto-> W -> F : C --> W ) |
| 11 |
10
|
adantr |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> F : C --> W ) |
| 12 |
11
|
adantr |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> F : C --> W ) |
| 13 |
|
simpr3 |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> B e. C ) |
| 14 |
12 13
|
ffvelcdmd |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` B ) e. W ) |
| 15 |
5
|
fveq2i |
|- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) |
| 16 |
|
stgrvtx |
|- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) |
| 17 |
4 16
|
ax-mp |
|- ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) |
| 18 |
6 15 17
|
3eqtri |
|- W = ( 0 ... N ) |
| 19 |
18
|
eleq2i |
|- ( ( F ` B ) e. W <-> ( F ` B ) e. ( 0 ... N ) ) |
| 20 |
|
fz0sn0fz1 |
|- ( N e. NN0 -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) ) |
| 21 |
4 20
|
ax-mp |
|- ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) |
| 22 |
21
|
eleq2i |
|- ( ( F ` B ) e. ( 0 ... N ) <-> ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) ) |
| 23 |
|
elun |
|- ( ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) <-> ( ( F ` B ) e. { 0 } \/ ( F ` B ) e. ( 1 ... N ) ) ) |
| 24 |
|
fvex |
|- ( F ` B ) e. _V |
| 25 |
24
|
elsn |
|- ( ( F ` B ) e. { 0 } <-> ( F ` B ) = 0 ) |
| 26 |
25
|
orbi1i |
|- ( ( ( F ` B ) e. { 0 } \/ ( F ` B ) e. ( 1 ... N ) ) <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) ) |
| 27 |
23 26
|
bitri |
|- ( ( F ` B ) e. ( { 0 } u. ( 1 ... N ) ) <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) ) |
| 28 |
19 22 27
|
3bitri |
|- ( ( F ` B ) e. W <-> ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) ) |
| 29 |
|
eqeq2 |
|- ( ( F ` X ) = 0 -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) ) |
| 30 |
29
|
adantl |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) ) |
| 31 |
30
|
adantr |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = ( F ` X ) <-> ( F ` B ) = 0 ) ) |
| 32 |
|
f1of1 |
|- ( F : C -1-1-onto-> W -> F : C -1-1-> W ) |
| 33 |
|
dff14a |
|- ( F : C -1-1-> W <-> ( F : C --> W /\ A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) ) |
| 34 |
|
simpl |
|- ( ( a = X /\ b = B ) -> a = X ) |
| 35 |
|
simpr |
|- ( ( a = X /\ b = B ) -> b = B ) |
| 36 |
34 35
|
neeq12d |
|- ( ( a = X /\ b = B ) -> ( a =/= b <-> X =/= B ) ) |
| 37 |
|
fveq2 |
|- ( a = X -> ( F ` a ) = ( F ` X ) ) |
| 38 |
37
|
adantr |
|- ( ( a = X /\ b = B ) -> ( F ` a ) = ( F ` X ) ) |
| 39 |
|
fveq2 |
|- ( b = B -> ( F ` b ) = ( F ` B ) ) |
| 40 |
39
|
adantl |
|- ( ( a = X /\ b = B ) -> ( F ` b ) = ( F ` B ) ) |
| 41 |
38 40
|
neeq12d |
|- ( ( a = X /\ b = B ) -> ( ( F ` a ) =/= ( F ` b ) <-> ( F ` X ) =/= ( F ` B ) ) ) |
| 42 |
36 41
|
imbi12d |
|- ( ( a = X /\ b = B ) -> ( ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) <-> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) ) |
| 43 |
42
|
rspc2gv |
|- ( ( X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) ) |
| 44 |
43
|
3adant1 |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) ) |
| 45 |
|
id |
|- ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) ) |
| 46 |
|
eqneqall |
|- ( ( F ` X ) = ( F ` B ) -> ( ( F ` X ) =/= ( F ` B ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 47 |
46
|
eqcoms |
|- ( ( F ` B ) = ( F ` X ) -> ( ( F ` X ) =/= ( F ` B ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 48 |
47
|
com12 |
|- ( ( F ` X ) =/= ( F ` B ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 49 |
45 48
|
syl6com |
|- ( X =/= B -> ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 50 |
49
|
3ad2ant1 |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( X =/= B -> ( F ` X ) =/= ( F ` B ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 51 |
44 50
|
syld |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 52 |
51
|
adantld |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F : C --> W /\ A. a e. C A. b e. C ( a =/= b -> ( F ` a ) =/= ( F ` b ) ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 53 |
33 52
|
biimtrid |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( F : C -1-1-> W -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 54 |
32 53
|
syl5com |
|- ( F : C -1-1-onto-> W -> ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 55 |
54
|
adantr |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( X =/= B /\ X e. C /\ B e. C ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) ) |
| 56 |
55
|
imp |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = ( F ` X ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 57 |
31 56
|
sylbird |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) = 0 -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 58 |
|
idd |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) e. ( 1 ... N ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 59 |
57 58
|
jaod |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( ( F ` B ) = 0 \/ ( F ` B ) e. ( 1 ... N ) ) -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 60 |
28 59
|
biimtrid |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( ( F ` B ) e. W -> ( F ` B ) e. ( 1 ... N ) ) ) |
| 61 |
14 60
|
mpd |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` B ) e. ( 1 ... N ) ) |
| 62 |
|
f1ofn |
|- ( F : C -1-1-onto-> W -> F Fn C ) |
| 63 |
62
|
adantr |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> F Fn C ) |
| 64 |
|
3simpc |
|- ( ( X =/= B /\ X e. C /\ B e. C ) -> ( X e. C /\ B e. C ) ) |
| 65 |
63 64
|
anim12i |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F Fn C /\ ( X e. C /\ B e. C ) ) ) |
| 66 |
|
3anass |
|- ( ( F Fn C /\ X e. C /\ B e. C ) <-> ( F Fn C /\ ( X e. C /\ B e. C ) ) ) |
| 67 |
65 66
|
sylibr |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F Fn C /\ X e. C /\ B e. C ) ) |
| 68 |
|
fnimapr |
|- ( ( F Fn C /\ X e. C /\ B e. C ) -> ( F " { X , B } ) = { ( F ` X ) , ( F ` B ) } ) |
| 69 |
67 68
|
syl |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F " { X , B } ) = { ( F ` X ) , ( F ` B ) } ) |
| 70 |
|
simpr |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( F ` X ) = 0 ) |
| 71 |
70
|
adantr |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F ` X ) = 0 ) |
| 72 |
71
|
preq1d |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> { ( F ` X ) , ( F ` B ) } = { 0 , ( F ` B ) } ) |
| 73 |
69 72
|
eqtrd |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> ( F " { X , B } ) = { 0 , ( F ` B ) } ) |
| 74 |
9 61 73
|
rspcedvdw |
|- ( ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( X =/= B /\ X e. C /\ B e. C ) ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) |
| 75 |
74
|
ex |
|- ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( X =/= B /\ X e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) ) |
| 76 |
|
neeq1 |
|- ( A = X -> ( A =/= B <-> X =/= B ) ) |
| 77 |
|
eleq1 |
|- ( A = X -> ( A e. C <-> X e. C ) ) |
| 78 |
76 77
|
3anbi12d |
|- ( A = X -> ( ( A =/= B /\ A e. C /\ B e. C ) <-> ( X =/= B /\ X e. C /\ B e. C ) ) ) |
| 79 |
|
preq1 |
|- ( A = X -> { A , B } = { X , B } ) |
| 80 |
79
|
imaeq2d |
|- ( A = X -> ( F " { A , B } ) = ( F " { X , B } ) ) |
| 81 |
80
|
eqeq1d |
|- ( A = X -> ( ( F " { A , B } ) = { 0 , z } <-> ( F " { X , B } ) = { 0 , z } ) ) |
| 82 |
81
|
rexbidv |
|- ( A = X -> ( E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } <-> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) ) |
| 83 |
78 82
|
imbi12d |
|- ( A = X -> ( ( ( A =/= B /\ A e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) <-> ( ( X =/= B /\ X e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { X , B } ) = { 0 , z } ) ) ) |
| 84 |
75 83
|
imbitrrid |
|- ( A = X -> ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> ( ( A =/= B /\ A e. C /\ B e. C ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) ) ) |
| 85 |
84
|
3imp |
|- ( ( A = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( A =/= B /\ A e. C /\ B e. C ) ) -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) |