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 e. NN0
isubgr3stgr.s 
|- S = ( StarGr ` N )
isubgr3stgr.w 
|- W = ( Vtx ` S )
isubgr3stgr.e 
|- E = ( Edg ` G )
isubgr3stgr.i 
|- I = ( Edg ` ( G ISubGr C ) )
isubgr3stgr.h 
|- H = ( i e. I |-> ( F " i ) )
Assertion isubgr3stgrlem8 
|- ( ( ( ( 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 ) ) )

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