| 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.f |
|- F = ( H u. { <. X , Y >. } ) |
| 5 |
|
f1oeq2 |
|- ( U = ( G NeighbVtx X ) -> ( H : U -1-1-onto-> R <-> H : ( G NeighbVtx X ) -1-1-onto-> R ) ) |
| 6 |
2 5
|
ax-mp |
|- ( H : U -1-1-onto-> R <-> H : ( G NeighbVtx X ) -1-1-onto-> R ) |
| 7 |
6
|
biimpi |
|- ( H : U -1-1-onto-> R -> H : ( G NeighbVtx X ) -1-1-onto-> R ) |
| 8 |
7
|
3ad2ant1 |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> H : ( G NeighbVtx X ) -1-1-onto-> R ) |
| 9 |
|
simpl |
|- ( ( Y e. W /\ Y e/ R ) -> Y e. W ) |
| 10 |
9
|
anim2i |
|- ( ( X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( X e. V /\ Y e. W ) ) |
| 11 |
10
|
3adant1 |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( X e. V /\ Y e. W ) ) |
| 12 |
|
nbgrnself2 |
|- X e/ ( G NeighbVtx X ) |
| 13 |
12
|
a1i |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> X e/ ( G NeighbVtx X ) ) |
| 14 |
|
simp3r |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> Y e/ R ) |
| 15 |
4
|
f1ounsn |
|- ( ( H : ( G NeighbVtx X ) -1-1-onto-> R /\ ( X e. V /\ Y e. W ) /\ ( X e/ ( G NeighbVtx X ) /\ Y e/ R ) ) -> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) ) |
| 16 |
8 11 13 14 15
|
syl112anc |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) ) |
| 17 |
1
|
dfclnbgr4 |
|- ( X e. V -> ( G ClNeighbVtx X ) = ( { X } u. ( G NeighbVtx X ) ) ) |
| 18 |
17
|
3ad2ant2 |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( G ClNeighbVtx X ) = ( { X } u. ( G NeighbVtx X ) ) ) |
| 19 |
|
uncom |
|- ( { X } u. ( G NeighbVtx X ) ) = ( ( G NeighbVtx X ) u. { X } ) |
| 20 |
18 19
|
eqtrdi |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( G ClNeighbVtx X ) = ( ( G NeighbVtx X ) u. { X } ) ) |
| 21 |
3 20
|
eqtrid |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> C = ( ( G NeighbVtx X ) u. { X } ) ) |
| 22 |
21
|
f1oeq2d |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> ( F : C -1-1-onto-> ( R u. { Y } ) <-> F : ( ( G NeighbVtx X ) u. { X } ) -1-1-onto-> ( R u. { Y } ) ) ) |
| 23 |
16 22
|
mpbird |
|- ( ( H : U -1-1-onto-> R /\ X e. V /\ ( Y e. W /\ Y e/ R ) ) -> F : C -1-1-onto-> ( R u. { Y } ) ) |