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