Metamath Proof Explorer

Theorem isubgr3stgrlem7

Description: Lemma 7 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 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 )

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 stgredgel 
 |-  ( N e. NN0 -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) )
11 4 10 mp1i 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) )
12 c0ex 
 |-  0 e. _V
13 12 a1i 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> 0 e. _V )
14 prssg 
 |-  ( ( 0 e. _V /\ y e. ( 1 ... N ) ) -> ( ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) <-> { 0 , y } C_ ( 0 ... N ) ) )
15 13 14 sylan 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) <-> { 0 , y } C_ ( 0 ... N ) ) )
16 f1ocnv 
 |-  ( F : C -1-1-onto-> W -> `' F : W -1-1-onto-> C )
17 f1ofn 
 |-  ( `' F : W -1-1-onto-> C -> `' F Fn W )
18 5 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) )
19 stgrvtx 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )
20 4 19 ax-mp 
 |-  ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N )
21 6 18 20 3eqtri 
 |-  W = ( 0 ... N )
22 21 fneq2i 
 |-  ( `' F Fn W <-> `' F Fn ( 0 ... N ) )
23 17 22 sylib 
 |-  ( `' F : W -1-1-onto-> C -> `' F Fn ( 0 ... N ) )
24 16 23 syl 
 |-  ( F : C -1-1-onto-> W -> `' F Fn ( 0 ... N ) )
25 24 ad2antrl 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> `' F Fn ( 0 ... N ) )
26 25 adantr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> `' F Fn ( 0 ... N ) )
27 26 anim1i 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) -> ( `' F Fn ( 0 ... N ) /\ ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) )
28 3anass 
 |-  ( ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) <-> ( `' F Fn ( 0 ... N ) /\ ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) )
29 27 28 sylibr 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) -> ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) )
30 29 ex 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( ( 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) -> ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) )
31 15 30 sylbird 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( { 0 , y } C_ ( 0 ... N ) -> ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) ) )
32 31 imp 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) )
33 fnimapr 
 |-  ( ( `' F Fn ( 0 ... N ) /\ 0 e. ( 0 ... N ) /\ y e. ( 0 ... N ) ) -> ( `' F " { 0 , y } ) = { ( `' F ` 0 ) , ( `' F ` y ) } )
34 32 33 syl 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> ( `' F " { 0 , y } ) = { ( `' F ` 0 ) , ( `' F ` y ) } )
35 1 clnbgrvtxel 
 |-  ( X e. V -> X e. ( G ClNeighbVtx X ) )
36 35 adantl 
 |-  ( ( G e. USGraph /\ X e. V ) -> X e. ( G ClNeighbVtx X ) )
37 36 3 eleqtrrdi 
 |-  ( ( G e. USGraph /\ X e. V ) -> X e. C )
38 simpl 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> F : C -1-1-onto-> W )
39 37 38 anim12ci 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( F : C -1-1-onto-> W /\ X e. C ) )
40 simprr 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( F ` X ) = 0 )
41 39 40 jca 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( ( F : C -1-1-onto-> W /\ X e. C ) /\ ( F ` X ) = 0 ) )
42 41 adantr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( ( F : C -1-1-onto-> W /\ X e. C ) /\ ( F ` X ) = 0 ) )
43 f1ocnvfv 
 |-  ( ( F : C -1-1-onto-> W /\ X e. C ) -> ( ( F ` X ) = 0 -> ( `' F ` 0 ) = X ) )
44 43 imp 
 |-  ( ( ( F : C -1-1-onto-> W /\ X e. C ) /\ ( F ` X ) = 0 ) -> ( `' F ` 0 ) = X )
45 42 44 syl 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( `' F ` 0 ) = X )
46 35 3 eleqtrrdi 
 |-  ( X e. V -> X e. C )
47 46 ad3antlr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> X e. C )
48 f1of 
 |-  ( `' F : W -1-1-onto-> C -> `' F : W --> C )
49 16 48 syl 
 |-  ( F : C -1-1-onto-> W -> `' F : W --> C )
50 49 ad2antrl 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> `' F : W --> C )
51 50 adantr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> `' F : W --> C )
52 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
53 52 sseli 
 |-  ( y e. ( 1 ... N ) -> y e. ( 0 ... N ) )
54 53 21 eleqtrrdi 
 |-  ( y e. ( 1 ... N ) -> y e. W )
55 54 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> y e. W )
56 51 55 ffvelcdmd 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( `' F ` y ) e. C )
57 47 56 jca 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( X e. C /\ ( `' F ` y ) e. C ) )
58 3 eleq2i 
 |-  ( ( `' F ` y ) e. C <-> ( `' F ` y ) e. ( G ClNeighbVtx X ) )
59 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
60 59 anim1i 
 |-  ( ( G e. USGraph /\ X e. V ) -> ( G e. UPGraph /\ X e. V ) )
61 60 ad2antrr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( G e. UPGraph /\ X e. V ) )
62 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx X ) C_ V
63 3 62 eqsstri 
 |-  C C_ V
64 63 56 sselid 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( `' F ` y ) e. V )
65 df-3an 
 |-  ( ( G e. UPGraph /\ X e. V /\ ( `' F ` y ) e. V ) <-> ( ( G e. UPGraph /\ X e. V ) /\ ( `' F ` y ) e. V ) )
66 61 64 65 sylanbrc 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( G e. UPGraph /\ X e. V /\ ( `' F ` y ) e. V ) )
67 66 ad2antrr 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( G e. UPGraph /\ X e. V /\ ( `' F ` y ) e. V ) )
68 1 7 clnbupgrel 
 |-  ( ( G e. UPGraph /\ X e. V /\ ( `' F ` y ) e. V ) -> ( ( `' F ` y ) e. ( G ClNeighbVtx X ) <-> ( ( `' F ` y ) = X \/ { ( `' F ` y ) , X } e. E ) ) )
69 67 68 syl 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( ( `' F ` y ) e. ( G ClNeighbVtx X ) <-> ( ( `' F ` y ) = X \/ { ( `' F ` y ) , X } e. E ) ) )
70 58 69 bitrid 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( ( `' F ` y ) e. C <-> ( ( `' F ` y ) = X \/ { ( `' F ` y ) , X } e. E ) ) )
71 eqeq2 
 |-  ( ( `' F ` 0 ) = X -> ( ( `' F ` y ) = ( `' F ` 0 ) <-> ( `' F ` y ) = X ) )
72 71 adantl 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( ( `' F ` y ) = ( `' F ` 0 ) <-> ( `' F ` y ) = X ) )
73 f1of1 
 |-  ( `' F : W -1-1-onto-> C -> `' F : W -1-1-> C )
74 16 73 syl 
 |-  ( F : C -1-1-onto-> W -> `' F : W -1-1-> C )
75 74 ad2antrl 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> `' F : W -1-1-> C )
76 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
77 4 76 ax-mp 
 |-  0 e. ( 0 ... N )
78 77 21 eleqtrri 
 |-  0 e. W
79 54 78 jctir 
 |-  ( y e. ( 1 ... N ) -> ( y e. W /\ 0 e. W ) )
80 f1veqaeq 
 |-  ( ( `' F : W -1-1-> C /\ ( y e. W /\ 0 e. W ) ) -> ( ( `' F ` y ) = ( `' F ` 0 ) -> y = 0 ) )
81 75 79 80 syl2an 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( ( `' F ` y ) = ( `' F ` 0 ) -> y = 0 ) )
82 elfznn 
 |-  ( y e. ( 1 ... N ) -> y e. NN )
83 nnne0 
 |-  ( y e. NN -> y =/= 0 )
84 eqneqall 
 |-  ( y = 0 -> ( y =/= 0 -> { X , ( `' F ` y ) } e. E ) )
85 83 84 syl5com 
 |-  ( y e. NN -> ( y = 0 -> { X , ( `' F ` y ) } e. E ) )
86 82 85 syl 
 |-  ( y e. ( 1 ... N ) -> ( y = 0 -> { X , ( `' F ` y ) } e. E ) )
87 86 adantl 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( y = 0 -> { X , ( `' F ` y ) } e. E ) )
88 81 87 syld 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( ( `' F ` y ) = ( `' F ` 0 ) -> { X , ( `' F ` y ) } e. E ) )
89 88 adantr 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( ( `' F ` y ) = ( `' F ` 0 ) -> { X , ( `' F ` y ) } e. E ) )
90 72 89 sylbird 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( ( `' F ` y ) = X -> { X , ( `' F ` y ) } e. E ) )
91 90 adantr 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( ( `' F ` y ) = X -> { X , ( `' F ` y ) } e. E ) )
92 prcom 
 |-  { ( `' F ` y ) , X } = { X , ( `' F ` y ) }
93 92 eleq1i 
 |-  ( { ( `' F ` y ) , X } e. E <-> { X , ( `' F ` y ) } e. E )
94 93 biimpi 
 |-  ( { ( `' F ` y ) , X } e. E -> { X , ( `' F ` y ) } e. E )
95 94 a1i 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( { ( `' F ` y ) , X } e. E -> { X , ( `' F ` y ) } e. E ) )
96 91 95 jaod 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( ( ( `' F ` y ) = X \/ { ( `' F ` y ) , X } e. E ) -> { X , ( `' F ` y ) } e. E ) )
97 70 96 sylbid 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ X e. C ) -> ( ( `' F ` y ) e. C -> { X , ( `' F ` y ) } e. E ) )
98 97 impr 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ ( X e. C /\ ( `' F ` y ) e. C ) ) -> { X , ( `' F ` y ) } e. E )
99 prssi 
 |-  ( ( X e. C /\ ( `' F ` y ) e. C ) -> { X , ( `' F ` y ) } C_ C )
100 99 adantl 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ ( X e. C /\ ( `' F ` y ) e. C ) ) -> { X , ( `' F ` y ) } C_ C )
101 98 100 jca 
 |-  ( ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) /\ ( X e. C /\ ( `' F ` y ) e. C ) ) -> ( { X , ( `' F ` y ) } e. E /\ { X , ( `' F ` y ) } C_ C ) )
102 57 101 mpidan 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( { X , ( `' F ` y ) } e. E /\ { X , ( `' F ` y ) } C_ C ) )
103 preq1 
 |-  ( ( `' F ` 0 ) = X -> { ( `' F ` 0 ) , ( `' F ` y ) } = { X , ( `' F ` y ) } )
104 103 eleq1d 
 |-  ( ( `' F ` 0 ) = X -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E <-> { X , ( `' F ` y ) } e. E ) )
105 103 sseq1d 
 |-  ( ( `' F ` 0 ) = X -> ( { ( `' F ` 0 ) , ( `' F ` y ) } C_ C <-> { X , ( `' F ` y ) } C_ C ) )
106 104 105 anbi12d 
 |-  ( ( `' F ` 0 ) = X -> ( ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) <-> ( { X , ( `' F ` y ) } e. E /\ { X , ( `' F ` y ) } C_ C ) ) )
107 106 adantl 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) <-> ( { X , ( `' F ` y ) } e. E /\ { X , ( `' F ` y ) } C_ C ) ) )
108 102 107 mpbird 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ ( `' F ` 0 ) = X ) -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) )
109 45 108 mpdan 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) )
110 109 adantr 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) )
111 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
112 111 ad3antrrr 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> G e. UHGraph )
113 63 a1i 
 |-  ( { 0 , y } C_ ( 0 ... N ) -> C C_ V )
114 eqid 
 |-  ( G ISubGr C ) = ( G ISubGr C )
115 1 7 114 8 isubgredg 
 |-  ( ( G e. UHGraph /\ C C_ V ) -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. I <-> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) ) )
116 112 113 115 syl2an 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. I <-> ( { ( `' F ` 0 ) , ( `' F ` y ) } e. E /\ { ( `' F ` 0 ) , ( `' F ` y ) } C_ C ) ) )
117 110 116 mpbird 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> { ( `' F ` 0 ) , ( `' F ` y ) } e. I )
118 34 117 eqeltrd 
 |-  ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) /\ { 0 , y } C_ ( 0 ... N ) ) -> ( `' F " { 0 , y } ) e. I )
119 118 ex 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( { 0 , y } C_ ( 0 ... N ) -> ( `' F " { 0 , y } ) e. I ) )
120 sseq1 
 |-  ( J = { 0 , y } -> ( J C_ ( 0 ... N ) <-> { 0 , y } C_ ( 0 ... N ) ) )
121 imaeq2 
 |-  ( J = { 0 , y } -> ( `' F " J ) = ( `' F " { 0 , y } ) )
122 121 eleq1d 
 |-  ( J = { 0 , y } -> ( ( `' F " J ) e. I <-> ( `' F " { 0 , y } ) e. I ) )
123 120 122 imbi12d 
 |-  ( J = { 0 , y } -> ( ( J C_ ( 0 ... N ) -> ( `' F " J ) e. I ) <-> ( { 0 , y } C_ ( 0 ... N ) -> ( `' F " { 0 , y } ) e. I ) ) )
124 119 123 syl5ibrcom 
 |-  ( ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ y e. ( 1 ... N ) ) -> ( J = { 0 , y } -> ( J C_ ( 0 ... N ) -> ( `' F " J ) e. I ) ) )
125 124 rexlimdva 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( E. y e. ( 1 ... N ) J = { 0 , y } -> ( J C_ ( 0 ... N ) -> ( `' F " J ) e. I ) ) )
126 125 impcomd 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) -> ( `' F " J ) e. I ) )
127 11 126 sylbid 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) -> ( `' F " J ) e. I ) )
128 127 3impia 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ J e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " J ) e. I )