Metamath Proof Explorer

Theorem isubgr3stgrlem6

Description: Lemma 6 for isubgr3stgr . (Contributed by AV, 24-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 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 ) ) )

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 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
11 10 adantr 
 |-  ( ( G e. USGraph /\ X e. V ) -> G e. UHGraph )
12 11 adantr 
 |-  ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> G e. UHGraph )
13 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx X ) C_ V
14 3 13 eqsstri 
 |-  C C_ V
15 14 a1i 
 |-  ( ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) -> C C_ V )
16 eqid 
 |-  ( G ISubGr C ) = ( G ISubGr C )
17 1 7 16 8 isubgredg 
 |-  ( ( G e. UHGraph /\ C C_ V ) -> ( i e. I <-> ( i e. E /\ i C_ C ) ) )
18 12 15 17 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 ) ) -> ( i e. I <-> ( i e. E /\ i C_ C ) ) )
19 f1of 
 |-  ( F : C -1-1-onto-> W -> F : C --> W )
20 5 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) )
21 stgrvtx 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )
22 4 21 ax-mp 
 |-  ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N )
23 6 20 22 3eqtri 
 |-  W = ( 0 ... N )
24 23 eqimssi 
 |-  W C_ ( 0 ... N )
25 24 a1i 
 |-  ( F : C -1-1-onto-> W -> W C_ ( 0 ... N ) )
26 19 25 fssd 
 |-  ( F : C -1-1-onto-> W -> F : C --> ( 0 ... N ) )
27 26 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 --> ( 0 ... N ) )
28 27 adantr 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> F : C --> ( 0 ... N ) )
29 28 fimassd 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( F " i ) C_ ( 0 ... N ) )
30 simplll 
 |-  ( ( ( ( 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 ) ) -> G e. USGraph )
31 simpl 
 |-  ( ( i e. E /\ i C_ C ) -> i e. E )
32 1 7 usgredg 
 |-  ( ( G e. USGraph /\ i e. E ) -> E. a e. V E. b e. V ( a =/= b /\ i = { a , b } ) )
33 30 31 32 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> E. a e. V E. b e. V ( a =/= b /\ i = { a , b } ) )
34 vex 
 |-  a e. _V
35 vex 
 |-  b e. _V
36 34 35 prss 
 |-  ( ( a e. C /\ b e. C ) <-> { a , b } C_ C )
37 elclnbgrelnbgr 
 |-  ( ( a e. ( G ClNeighbVtx X ) /\ a =/= X ) -> a e. ( G NeighbVtx X ) )
38 37 expcom 
 |-  ( a =/= X -> ( a e. ( G ClNeighbVtx X ) -> a e. ( G NeighbVtx X ) ) )
39 3 eleq2i 
 |-  ( a e. C <-> a e. ( G ClNeighbVtx X ) )
40 2 eleq2i 
 |-  ( a e. U <-> a e. ( G NeighbVtx X ) )
41 38 39 40 3imtr4g 
 |-  ( a =/= X -> ( a e. C -> a e. U ) )
42 elclnbgrelnbgr 
 |-  ( ( b e. ( G ClNeighbVtx X ) /\ b =/= X ) -> b e. ( G NeighbVtx X ) )
43 42 expcom 
 |-  ( b =/= X -> ( b e. ( G ClNeighbVtx X ) -> b e. ( G NeighbVtx X ) ) )
44 3 eleq2i 
 |-  ( b e. C <-> b e. ( G ClNeighbVtx X ) )
45 2 eleq2i 
 |-  ( b e. U <-> b e. ( G NeighbVtx X ) )
46 43 44 45 3imtr4g 
 |-  ( b =/= X -> ( b e. C -> b e. U ) )
47 41 46 im2anan9r 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( a e. C /\ b e. C ) -> ( a e. U /\ b e. U ) ) )
48 47 imp 
 |-  ( ( ( b =/= X /\ a =/= X ) /\ ( a e. C /\ b e. C ) ) -> ( a e. U /\ b e. U ) )
49 48 3adant3 
 |-  ( ( ( b =/= X /\ a =/= X ) /\ ( a e. C /\ b e. C ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( a e. U /\ b e. U ) )
50 preq1 
 |-  ( x = a -> { x , y } = { a , y } )
51 eqidd 
 |-  ( x = a -> E = E )
52 50 51 neleq12d 
 |-  ( x = a -> ( { x , y } e/ E <-> { a , y } e/ E ) )
53 preq2 
 |-  ( y = b -> { a , y } = { a , b } )
54 eqidd 
 |-  ( y = b -> E = E )
55 53 54 neleq12d 
 |-  ( y = b -> ( { a , y } e/ E <-> { a , b } e/ E ) )
56 52 55 rspc2v 
 |-  ( ( a e. U /\ b e. U ) -> ( A. x e. U A. y e. U { x , y } e/ E -> { a , b } e/ E ) )
57 49 56 syl 
 |-  ( ( ( b =/= X /\ a =/= X ) /\ ( a e. C /\ b e. C ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( A. x e. U A. y e. U { x , y } e/ E -> { a , b } e/ E ) )
58 pm2.24nel 
 |-  ( { a , b } e. E -> ( { a , b } e/ E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
59 58 adantl 
 |-  ( ( a =/= b /\ { a , b } e. E ) -> ( { a , b } e/ E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
60 59 3ad2ant3 
 |-  ( ( ( b =/= X /\ a =/= X ) /\ ( a e. C /\ b e. C ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( { a , b } e/ E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
61 57 60 syld 
 |-  ( ( ( b =/= X /\ a =/= X ) /\ ( a e. C /\ b e. C ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( A. x e. U A. y e. U { x , y } e/ E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
62 61 3exp 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( a e. C /\ b e. C ) -> ( ( a =/= b /\ { a , b } e. E ) -> ( A. x e. U A. y e. U { x , y } e/ E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
63 62 com24 
 |-  ( ( b =/= X /\ a =/= X ) -> ( A. x e. U A. y e. U { x , y } e/ E -> ( ( a =/= b /\ { a , b } e. E ) -> ( ( a e. C /\ b e. C ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
64 63 adantld 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) -> ( ( a =/= b /\ { a , b } e. E ) -> ( ( a e. C /\ b e. C ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
65 64 adantld 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> ( ( a =/= b /\ { a , b } e. E ) -> ( ( a e. C /\ b e. C ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
66 65 adantrd 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( ( ( 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 ) ) -> ( ( a =/= b /\ { a , b } e. E ) -> ( ( a e. C /\ b e. C ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
67 66 imp4c 
 |-  ( ( b =/= X /\ a =/= X ) -> ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
68 simpl 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> b = X )
69 simpllr 
 |-  ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) )
70 69 adantl 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) )
71 simplrl 
 |-  ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> a =/= b )
72 71 necomd 
 |-  ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> b =/= a )
73 72 adantl 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> b =/= a )
74 simprrr 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> b e. C )
75 simprrl 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> a e. C )
76 1 2 3 4 5 6 7 isubgr3stgrlem4 
 |-  ( ( b = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( b =/= a /\ b e. C /\ a e. C ) ) -> E. z e. ( 1 ... N ) ( F " { b , a } ) = { 0 , z } )
77 68 70 73 74 75 76 syl113anc 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> E. z e. ( 1 ... N ) ( F " { b , a } ) = { 0 , z } )
78 prcom 
 |-  { a , b } = { b , a }
79 78 imaeq2i 
 |-  ( F " { a , b } ) = ( F " { b , a } )
80 79 eqeq1i 
 |-  ( ( F " { a , b } ) = { 0 , z } <-> ( F " { b , a } ) = { 0 , z } )
81 80 rexbii 
 |-  ( E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } <-> E. z e. ( 1 ... N ) ( F " { b , a } ) = { 0 , z } )
82 77 81 sylibr 
 |-  ( ( b = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } )
83 82 ex 
 |-  ( b = X -> ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
84 simpl 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> a = X )
85 69 adantl 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) )
86 71 adantl 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> a =/= b )
87 simprrl 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> a e. C )
88 simprrr 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> b e. C )
89 1 2 3 4 5 6 7 isubgr3stgrlem4 
 |-  ( ( a = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ ( a =/= b /\ a e. C /\ b e. C ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } )
90 84 85 86 87 88 89 syl113anc 
 |-  ( ( a = X /\ ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } )
91 90 ex 
 |-  ( a = X -> ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
92 67 83 91 pm2.61iine 
 |-  ( ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) /\ ( a e. C /\ b e. C ) ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } )
93 92 ex 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( ( a e. C /\ b e. C ) -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
94 36 93 biimtrrid 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ { a , b } e. E ) ) -> ( { a , b } C_ C -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
95 94 exp32 
 |-  ( ( ( ( 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 ) ) -> ( a =/= b -> ( { a , b } e. E -> ( { a , b } C_ C -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
96 95 adantrd 
 |-  ( ( ( ( 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 ) ) -> ( ( a =/= b /\ i = { a , b } ) -> ( { a , b } e. E -> ( { a , b } C_ C -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
97 96 imp 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ i = { a , b } ) ) -> ( { a , b } e. E -> ( { a , b } C_ C -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) )
98 97 com23 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ i = { a , b } ) ) -> ( { a , b } C_ C -> ( { a , b } e. E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) )
99 sseq1 
 |-  ( i = { a , b } -> ( i C_ C <-> { a , b } C_ C ) )
100 eleq1 
 |-  ( i = { a , b } -> ( i e. E <-> { a , b } e. E ) )
101 imaeq2 
 |-  ( i = { a , b } -> ( F " i ) = ( F " { a , b } ) )
102 101 eqeq1d 
 |-  ( i = { a , b } -> ( ( F " i ) = { 0 , z } <-> ( F " { a , b } ) = { 0 , z } ) )
103 102 rexbidv 
 |-  ( i = { a , b } -> ( E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } <-> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) )
104 100 103 imbi12d 
 |-  ( i = { a , b } -> ( ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) <-> ( { a , b } e. E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) )
105 99 104 imbi12d 
 |-  ( i = { a , b } -> ( ( i C_ C -> ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) <-> ( { a , b } C_ C -> ( { a , b } e. E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
106 105 adantl 
 |-  ( ( a =/= b /\ i = { a , b } ) -> ( ( i C_ C -> ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) <-> ( { a , b } C_ C -> ( { a , b } e. E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
107 106 adantl 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ i = { a , b } ) ) -> ( ( i C_ C -> ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) <-> ( { a , b } C_ C -> ( { a , b } e. E -> E. z e. ( 1 ... N ) ( F " { a , b } ) = { 0 , z } ) ) ) )
108 98 107 mpbird 
 |-  ( ( ( ( ( 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 ) ) /\ ( a =/= b /\ i = { a , b } ) ) -> ( i C_ C -> ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) )
109 108 ex 
 |-  ( ( ( ( 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 ) ) -> ( ( a =/= b /\ i = { a , b } ) -> ( i C_ C -> ( i e. E -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) ) )
110 109 com24 
 |-  ( ( ( ( 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 ) ) -> ( i e. E -> ( i C_ C -> ( ( a =/= b /\ i = { a , b } ) -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) ) )
111 110 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( ( a =/= b /\ i = { a , b } ) -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) )
112 111 a1d 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( ( a e. V /\ b e. V ) -> ( ( a =/= b /\ i = { a , b } ) -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) )
113 112 rexlimdvv 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( E. a e. V E. b e. V ( a =/= b /\ i = { a , b } ) -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) )
114 33 113 mpd 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } )
115 stgredgel 
 |-  ( N e. NN0 -> ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) )
116 4 115 ax-mp 
 |-  ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) )
117 29 114 116 sylanbrc 
 |-  ( ( ( ( ( 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 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) )
118 18 117 sylbida 
 |-  ( ( ( ( ( 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 ) ) /\ i e. I ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) )
119 118 9 fmptd 
 |-  ( ( ( ( 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 ) ) )