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 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 isubgr3stgrlem7 Could not format assertion : 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 |-

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