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