Metamath Proof Explorer


Theorem isubgr3stgrlem4

Description: Lemma 4 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
Assertion 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

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 preq2 z = F B 0 z = 0 F B
9 8 eqeq2d z = F B F X B = 0 z F X B = 0 F B
10 f1of F : C 1-1 onto W F : C W
11 10 adantr F : C 1-1 onto W F X = 0 F : C W
12 11 adantr F : C 1-1 onto W F X = 0 X B X C B C F : C W
13 simpr3 F : C 1-1 onto W F X = 0 X B X C B C B C
14 12 13 ffvelcdmd F : C 1-1 onto W F X = 0 X B X C B C F B W
15 5 fveq2i Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
16 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 |-
17 4 16 ax-mp Could not format ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) : No typesetting found for |- ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) with typecode |-
18 6 15 17 3eqtri W = 0 N
19 18 eleq2i F B W F B 0 N
20 fz0sn0fz1 N 0 0 N = 0 1 N
21 4 20 ax-mp 0 N = 0 1 N
22 21 eleq2i F B 0 N F B 0 1 N
23 elun F B 0 1 N F B 0 F B 1 N
24 fvex F B V
25 24 elsn F B 0 F B = 0
26 25 orbi1i F B 0 F B 1 N F B = 0 F B 1 N
27 23 26 bitri F B 0 1 N F B = 0 F B 1 N
28 19 22 27 3bitri F B W F B = 0 F B 1 N
29 eqeq2 F X = 0 F B = F X F B = 0
30 29 adantl F : C 1-1 onto W F X = 0 F B = F X F B = 0
31 30 adantr F : C 1-1 onto W F X = 0 X B X C B C F B = F X F B = 0
32 f1of1 F : C 1-1 onto W F : C 1-1 W
33 dff14a F : C 1-1 W F : C W a C b C a b F a F b
34 simpl a = X b = B a = X
35 simpr a = X b = B b = B
36 34 35 neeq12d a = X b = B a b X B
37 fveq2 a = X F a = F X
38 37 adantr a = X b = B F a = F X
39 fveq2 b = B F b = F B
40 39 adantl a = X b = B F b = F B
41 38 40 neeq12d a = X b = B F a F b F X F B
42 36 41 imbi12d a = X b = B a b F a F b X B F X F B
43 42 rspc2gv X C B C a C b C a b F a F b X B F X F B
44 43 3adant1 X B X C B C a C b C a b F a F b X B F X F B
45 id X B F X F B X B F X F B
46 eqneqall F X = F B F X F B F B 1 N
47 46 eqcoms F B = F X F X F B F B 1 N
48 47 com12 F X F B F B = F X F B 1 N
49 45 48 syl6com X B X B F X F B F B = F X F B 1 N
50 49 3ad2ant1 X B X C B C X B F X F B F B = F X F B 1 N
51 44 50 syld X B X C B C a C b C a b F a F b F B = F X F B 1 N
52 51 adantld X B X C B C F : C W a C b C a b F a F b F B = F X F B 1 N
53 33 52 biimtrid X B X C B C F : C 1-1 W F B = F X F B 1 N
54 32 53 syl5com F : C 1-1 onto W X B X C B C F B = F X F B 1 N
55 54 adantr F : C 1-1 onto W F X = 0 X B X C B C F B = F X F B 1 N
56 55 imp F : C 1-1 onto W F X = 0 X B X C B C F B = F X F B 1 N
57 31 56 sylbird F : C 1-1 onto W F X = 0 X B X C B C F B = 0 F B 1 N
58 idd F : C 1-1 onto W F X = 0 X B X C B C F B 1 N F B 1 N
59 57 58 jaod F : C 1-1 onto W F X = 0 X B X C B C F B = 0 F B 1 N F B 1 N
60 28 59 biimtrid F : C 1-1 onto W F X = 0 X B X C B C F B W F B 1 N
61 14 60 mpd F : C 1-1 onto W F X = 0 X B X C B C F B 1 N
62 f1ofn F : C 1-1 onto W F Fn C
63 62 adantr F : C 1-1 onto W F X = 0 F Fn C
64 3simpc X B X C B C X C B C
65 63 64 anim12i F : C 1-1 onto W F X = 0 X B X C B C F Fn C X C B C
66 3anass F Fn C X C B C F Fn C X C B C
67 65 66 sylibr F : C 1-1 onto W F X = 0 X B X C B C F Fn C X C B C
68 fnimapr F Fn C X C B C F X B = F X F B
69 67 68 syl F : C 1-1 onto W F X = 0 X B X C B C F X B = F X F B
70 simpr F : C 1-1 onto W F X = 0 F X = 0
71 70 adantr F : C 1-1 onto W F X = 0 X B X C B C F X = 0
72 71 preq1d F : C 1-1 onto W F X = 0 X B X C B C F X F B = 0 F B
73 69 72 eqtrd F : C 1-1 onto W F X = 0 X B X C B C F X B = 0 F B
74 9 61 73 rspcedvdw F : C 1-1 onto W F X = 0 X B X C B C z 1 N F X B = 0 z
75 74 ex F : C 1-1 onto W F X = 0 X B X C B C z 1 N F X B = 0 z
76 neeq1 A = X A B X B
77 eleq1 A = X A C X C
78 76 77 3anbi12d A = X A B A C B C X B X C B C
79 preq1 A = X A B = X B
80 79 imaeq2d A = X F A B = F X B
81 80 eqeq1d A = X F A B = 0 z F X B = 0 z
82 81 rexbidv A = X z 1 N F A B = 0 z z 1 N F X B = 0 z
83 78 82 imbi12d A = X A B A C B C z 1 N F A B = 0 z X B X C B C z 1 N F X B = 0 z
84 75 83 imbitrrid 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
85 84 3imp 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