Metamath Proof Explorer


Theorem isubgr3stgrlem8

Description: Lemma 8 for isubgr3stgr . (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v V = Vtx G
isubgr3stgr.u U = G NeighbVtx X
isubgr3stgr.c C = G ClNeighbVtx X
isubgr3stgr.n N 0
isubgr3stgr.s No typesetting found for |- S = ( StarGr ` N ) with typecode |-
isubgr3stgr.w W = Vtx S
isubgr3stgr.e E = Edg G
isubgr3stgr.i I = Edg G ISubGr C
isubgr3stgr.h H = i I F i
Assertion isubgr3stgrlem8 Could not format assertion : 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 |-

Proof

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 0
5 isubgr3stgr.s Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |-
6 isubgr3stgr.w W = Vtx S
7 isubgr3stgr.e E = Edg G
8 isubgr3stgr.i I = Edg G ISubGr C
9 isubgr3stgr.h H = i I F i
10 imaeq2 i = k F i = F k
11 10 cbvmptv i I F i = k I F k
12 9 11 eqtri H = k I F k
13 f1of F : C 1-1 onto W F : C W
14 13 ad2antrl G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 F : C W
15 1 2 3 4 5 6 7 8 9 isubgr3stgrlem5 F : C W k I H k = F k
16 14 15 sylan G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 k I H k = F k
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 F : C 1-1 onto W F : C onto W
23 22 ad2antrl G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 F : C onto W
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 F : C onto W j W F F -1 j = j
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 k = F -1 j F k = F F -1 j
36 35 eqcomd k = F -1 j F F -1 j = F k
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 j = F k F -1 j = F -1 F k
39 f1of1 F : C 1-1 onto W F : C 1-1 W
40 39 ad2antrl G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 F : C 1-1 W
41 usgruhgr G USGraph G UHGraph
42 41 ad2antrr G USGraph X V U = N x U y U x y E G UHGraph
43 1 clnbgrssvtx G ClNeighbVtx X V
44 3 43 eqsstri C V
45 44 a1i F : C 1-1 onto W F X = 0 C V
46 eqid Edg G = Edg G
47 eqid G ISubGr C = G ISubGr C
48 1 46 47 8 isubgredg G UHGraph C V k I k Edg G k C
49 42 45 48 syl2an G USGraph X V U = N x U y U x y E F : C 1-1 onto W F X = 0 k I k Edg G k C
50 simpr k Edg G k C k C
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 F : C 1-1 W k C F -1 F k = k
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 |-