Metamath Proof Explorer


Theorem numclwwlk1lem2fo

Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v V = Vtx G
extwwlkfab.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
extwwlkfab.f F = X ClWWalksNOn G N 2
numclwwlk.t T = u X C N u prefix N 2 u N 1
Assertion numclwwlk1lem2fo G USGraph X V N 3 T : X C N onto F × G NeighbVtx X

Proof

Step Hyp Ref Expression
1 extwwlkfab.v V = Vtx G
2 extwwlkfab.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
3 extwwlkfab.f F = X ClWWalksNOn G N 2
4 numclwwlk.t T = u X C N u prefix N 2 u N 1
5 1 2 3 4 numclwwlk1lem2f G USGraph X V N 3 T : X C N F × G NeighbVtx X
6 elxp p F × G NeighbVtx X a b p = a b a F b G NeighbVtx X
7 1 2 3 numclwwlk1lem2foa G USGraph X V N 3 a F b G NeighbVtx X a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N
8 7 com12 a F b G NeighbVtx X G USGraph X V N 3 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N
9 8 adantl p = a b a F b G NeighbVtx X G USGraph X V N 3 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N
10 9 imp p = a b a F b G NeighbVtx X G USGraph X V N 3 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N
11 simpl a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N
12 fveq2 x = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ T x = T a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩
13 12 eqeq2d x = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ p = T x p = T a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩
14 1 2 3 4 numclwwlk1lem2fv a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N T a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
15 14 adantr a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 T a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
16 15 eqeq2d a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 p = T a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ p = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
17 13 16 sylan9bbr a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 x = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ p = T x p = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
18 simprll a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 p = a b
19 1 nbgrisvtx b G NeighbVtx X b V
20 3 eleq2i a F a X ClWWalksNOn G N 2
21 uz3m2nn N 3 N 2
22 21 nnne0d N 3 N 2 0
23 22 3ad2ant3 G USGraph X V N 3 N 2 0
24 eqid Edg G = Edg G
25 1 24 clwwlknonel N 2 0 a X ClWWalksNOn G N 2 a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X
26 23 25 syl G USGraph X V N 3 a X ClWWalksNOn G N 2 a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X
27 20 26 syl5bb G USGraph X V N 3 a F a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X
28 df-3an a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X
29 27 28 bitrdi G USGraph X V N 3 a F a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X
30 simplll a Word V a = N 2 X V N 3 b V a Word V
31 s1cl X V ⟨“ X ”⟩ Word V
32 31 adantr X V N 3 ⟨“ X ”⟩ Word V
33 32 adantl a Word V a = N 2 X V N 3 ⟨“ X ”⟩ Word V
34 33 adantr a Word V a = N 2 X V N 3 b V ⟨“ X ”⟩ Word V
35 s1cl b V ⟨“ b ”⟩ Word V
36 35 adantl a Word V a = N 2 X V N 3 b V ⟨“ b ”⟩ Word V
37 ccatass a Word V ⟨“ X ”⟩ Word V ⟨“ b ”⟩ Word V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩
38 37 oveq1d a Word V ⟨“ X ”⟩ Word V ⟨“ b ”⟩ Word V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2
39 30 34 36 38 syl3anc a Word V a = N 2 X V N 3 b V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2
40 ccatcl ⟨“ X ”⟩ Word V ⟨“ b ”⟩ Word V ⟨“ X ”⟩ ++ ⟨“ b ”⟩ Word V
41 33 35 40 syl2an a Word V a = N 2 X V N 3 b V ⟨“ X ”⟩ ++ ⟨“ b ”⟩ Word V
42 simpr a Word V a = N 2 a = N 2
43 42 eqcomd a Word V a = N 2 N 2 = a
44 43 adantr a Word V a = N 2 X V N 3 N 2 = a
45 44 adantr a Word V a = N 2 X V N 3 b V N 2 = a
46 pfxccatid a Word V ⟨“ X ”⟩ ++ ⟨“ b ”⟩ Word V N 2 = a a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 = a
47 30 41 45 46 syl3anc a Word V a = N 2 X V N 3 b V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 = a
48 39 47 eqtr2d a Word V a = N 2 X V N 3 b V a = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2
49 1e2m1 1 = 2 1
50 49 a1i N 3 1 = 2 1
51 50 oveq2d N 3 N 1 = N 2 1
52 eluzelcn N 3 N
53 2cnd N 3 2
54 1cnd N 3 1
55 52 53 54 subsubd N 3 N 2 1 = N - 2 + 1
56 51 55 eqtrd N 3 N 1 = N - 2 + 1
57 56 adantl X V N 3 N 1 = N - 2 + 1
58 57 adantl a Word V a = N 2 X V N 3 N 1 = N - 2 + 1
59 58 adantr a Word V a = N 2 X V N 3 b V N 1 = N - 2 + 1
60 59 fveq2d a Word V a = N 2 X V N 3 b V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1 = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N - 2 + 1
61 simpll a Word V a = N 2 X V N 3 b V a Word V a = N 2
62 simprl a Word V a = N 2 X V N 3 X V
63 62 anim1i a Word V a = N 2 X V N 3 b V X V b V
64 ccatw2s1p2 a Word V a = N 2 X V b V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N - 2 + 1 = b
65 61 63 64 syl2anc a Word V a = N 2 X V N 3 b V a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N - 2 + 1 = b
66 60 65 eqtr2d a Word V a = N 2 X V N 3 b V b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
67 48 66 opeq12d a Word V a = N 2 X V N 3 b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
68 67 exp31 a Word V a = N 2 X V N 3 b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
69 68 3ad2antl1 a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 X V N 3 b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
70 69 adantr a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X X V N 3 b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
71 70 com12 X V N 3 a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
72 71 3adant1 G USGraph X V N 3 a Word V i 0 ..^ a 1 a i a i + 1 Edg G lastS a a 0 Edg G a = N 2 a 0 = X b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
73 29 72 sylbid G USGraph X V N 3 a F b V a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
74 73 com23 G USGraph X V N 3 b V a F a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
75 19 74 syl5 G USGraph X V N 3 b G NeighbVtx X a F a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
76 75 com13 a F b G NeighbVtx X G USGraph X V N 3 a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
77 76 imp a F b G NeighbVtx X G USGraph X V N 3 a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
78 77 adantl p = a b a F b G NeighbVtx X G USGraph X V N 3 a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
79 78 imp p = a b a F b G NeighbVtx X G USGraph X V N 3 a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
80 79 adantl a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 a b = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
81 18 80 eqtrd a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 p = a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ prefix N 2 a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ N 1
82 11 17 81 rspcedvd a ++ ⟨“ X ”⟩ ++ ⟨“ b ”⟩ X C N p = a b a F b G NeighbVtx X G USGraph X V N 3 x X C N p = T x
83 10 82 mpancom p = a b a F b G NeighbVtx X G USGraph X V N 3 x X C N p = T x
84 83 ex p = a b a F b G NeighbVtx X G USGraph X V N 3 x X C N p = T x
85 84 exlimivv a b p = a b a F b G NeighbVtx X G USGraph X V N 3 x X C N p = T x
86 6 85 sylbi p F × G NeighbVtx X G USGraph X V N 3 x X C N p = T x
87 86 impcom G USGraph X V N 3 p F × G NeighbVtx X x X C N p = T x
88 87 ralrimiva G USGraph X V N 3 p F × G NeighbVtx X x X C N p = T x
89 dffo3 T : X C N onto F × G NeighbVtx X T : X C N F × G NeighbVtx X p F × G NeighbVtx X x X C N p = T x
90 5 88 89 sylanbrc G USGraph X V N 3 T : X C N onto F × G NeighbVtx X