| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isubgr3stgr.v |
|
| 2 |
|
isubgr3stgr.u |
|
| 3 |
|
isubgr3stgr.c |
|
| 4 |
|
isubgr3stgr.n |
|
| 5 |
|
isubgr3stgr.s |
Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |- |
| 6 |
|
isubgr3stgr.w |
|
| 7 |
|
isubgr3stgr.e |
|
| 8 |
|
isubgr3stgr.i |
|
| 9 |
|
isubgr3stgr.h |
|
| 10 |
|
imaeq2 |
|
| 11 |
10
|
cbvmptv |
|
| 12 |
9 11
|
eqtri |
|
| 13 |
|
f1of |
|
| 14 |
13
|
ad2antrl |
|
| 15 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem5 |
|
| 16 |
14 15
|
sylan |
|
| 17 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem6 |
Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I --> ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I --> ( Edg ` ( StarGr ` N ) ) ) with typecode |- |
| 18 |
17
|
ffvelcdmda |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ k e. I ) -> ( H ` k ) e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ k e. I ) -> ( H ` k ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode |- |
| 19 |
16 18
|
eqeltrrd |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ k e. I ) -> ( F " k ) e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ k e. I ) -> ( F " k ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode |- |
| 20 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem7 |
Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) : No typesetting found for |- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) with typecode |- |
| 21 |
20
|
ad4ant134 |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) with typecode |- |
| 22 |
|
f1ofo |
|
| 23 |
22
|
ad2antrl |
|
| 24 |
|
stgrusgra |
Could not format ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |- |
| 25 |
4 24
|
mp1i |
Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( StarGr ` N ) e. USGraph ) with typecode |- |
| 26 |
|
simpr |
Could not format ( ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j e. ( Edg ` ( StarGr ` N ) ) ) with typecode |- |
| 27 |
5
|
fveq2i |
Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode |- |
| 28 |
6 27
|
eqtri |
Could not format W = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- W = ( Vtx ` ( StarGr ` N ) ) with typecode |- |
| 29 |
|
eqid |
Could not format ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) : No typesetting found for |- ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) with typecode |- |
| 30 |
28 29
|
edgssv2 |
Could not format ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( j C_ W /\ ( # ` j ) = 2 ) ) : No typesetting found for |- ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( j C_ W /\ ( # ` j ) = 2 ) ) with typecode |- |
| 31 |
30
|
simpld |
Could not format ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j C_ W ) : No typesetting found for |- ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j C_ W ) with typecode |- |
| 32 |
25 26 31
|
syl2an |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> j C_ W ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> j C_ W ) with typecode |- |
| 33 |
|
foimacnv |
|
| 34 |
23 32 33
|
syl2an2r |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( F " ( `' F " j ) ) = j ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( F " ( `' F " j ) ) = j ) with typecode |- |
| 35 |
|
imaeq2 |
|
| 36 |
35
|
eqcomd |
|
| 37 |
34 36
|
sylan9req |
Could not format ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ k = ( `' F " j ) ) -> j = ( F " k ) ) : No typesetting found for |- ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ k = ( `' F " j ) ) -> j = ( F " k ) ) with typecode |- |
| 38 |
|
imaeq2 |
|
| 39 |
|
f1of1 |
|
| 40 |
39
|
ad2antrl |
|
| 41 |
|
usgruhgr |
|
| 42 |
41
|
ad2antrr |
|
| 43 |
1
|
clnbgrssvtx |
|
| 44 |
3 43
|
eqsstri |
|
| 45 |
44
|
a1i |
|
| 46 |
|
eqid |
|
| 47 |
|
eqid |
|
| 48 |
1 46 47 8
|
isubgredg |
|
| 49 |
42 45 48
|
syl2an |
|
| 50 |
|
simpr |
|
| 51 |
50
|
a1d |
Could not format ( ( k e. ( Edg ` G ) /\ k C_ C ) -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) : No typesetting found for |- ( ( k e. ( Edg ` G ) /\ k C_ C ) -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) with typecode |- |
| 52 |
49 51
|
biimtrdi |
Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( k e. I -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( k e. I -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) ) with typecode |- |
| 53 |
52
|
imp32 |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> k C_ C ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> k C_ C ) with typecode |- |
| 54 |
|
f1imacnv |
|
| 55 |
40 53 54
|
syl2an2r |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( `' F " ( F " k ) ) = k ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( `' F " ( F " k ) ) = k ) with typecode |- |
| 56 |
38 55
|
sylan9eqr |
Could not format ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> ( `' F " j ) = k ) : No typesetting found for |- ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> ( `' F " j ) = k ) with typecode |- |
| 57 |
56
|
eqcomd |
Could not format ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> k = ( `' F " j ) ) : No typesetting found for |- ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> k = ( `' F " j ) ) with typecode |- |
| 58 |
37 57
|
impbida |
Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( k = ( `' F " j ) <-> j = ( F " k ) ) ) : No typesetting found for |- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( k = ( `' F " j ) <-> j = ( F " k ) ) ) with typecode |- |
| 59 |
12 19 21 58
|
f1o2d |
Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) with typecode |- |