Metamath Proof Explorer


Theorem numclwlk2lem2f1o

Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Proof shortened by AV, 17-Mar-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses numclwwlk.v V = Vtx G
numclwwlk.q Q = v V , n w n WWalksN G | w 0 = v lastS w v
numclwwlk.h H = v V , n 2 w v ClWWalksNOn G n | w n 2 v
numclwwlk.r R = x X H N + 2 x prefix N + 1
Assertion numclwlk2lem2f1o G FriendGraph X V N R : X H N + 2 1-1 onto X Q N

Proof

Step Hyp Ref Expression
1 numclwwlk.v V = Vtx G
2 numclwwlk.q Q = v V , n w n WWalksN G | w 0 = v lastS w v
3 numclwwlk.h H = v V , n 2 w v ClWWalksNOn G n | w n 2 v
4 numclwwlk.r R = x X H N + 2 x prefix N + 1
5 eleq1w y = x y X H N + 2 x X H N + 2
6 fveq2 y = x R y = R x
7 oveq1 y = x y prefix N + 1 = x prefix N + 1
8 6 7 eqeq12d y = x R y = y prefix N + 1 R x = x prefix N + 1
9 5 8 imbi12d y = x y X H N + 2 R y = y prefix N + 1 x X H N + 2 R x = x prefix N + 1
10 9 imbi2d y = x X V N y X H N + 2 R y = y prefix N + 1 X V N x X H N + 2 R x = x prefix N + 1
11 1 2 3 4 numclwlk2lem2fv X V N y X H N + 2 R y = y prefix N + 1
12 10 11 chvarvv X V N x X H N + 2 R x = x prefix N + 1
13 12 3adant1 G FriendGraph X V N x X H N + 2 R x = x prefix N + 1
14 13 imp G FriendGraph X V N x X H N + 2 R x = x prefix N + 1
15 1 2 3 4 numclwlk2lem2f G FriendGraph X V N R : X H N + 2 X Q N
16 15 ffvelrnda G FriendGraph X V N x X H N + 2 R x X Q N
17 14 16 eqeltrrd G FriendGraph X V N x X H N + 2 x prefix N + 1 X Q N
18 17 ralrimiva G FriendGraph X V N x X H N + 2 x prefix N + 1 X Q N
19 1 2 3 numclwwlk2lem1 G FriendGraph X V N u X Q N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2
20 19 imp G FriendGraph X V N u X Q N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2
21 1 2 numclwwlkovq X V N X Q N = w N WWalksN G | w 0 = X lastS w X
22 21 eleq2d X V N u X Q N u w N WWalksN G | w 0 = X lastS w X
23 22 3adant1 G FriendGraph X V N u X Q N u w N WWalksN G | w 0 = X lastS w X
24 fveq1 w = u w 0 = u 0
25 24 eqeq1d w = u w 0 = X u 0 = X
26 fveq2 w = u lastS w = lastS u
27 26 neeq1d w = u lastS w X lastS u X
28 25 27 anbi12d w = u w 0 = X lastS w X u 0 = X lastS u X
29 28 elrab u w N WWalksN G | w 0 = X lastS w X u N WWalksN G u 0 = X lastS u X
30 23 29 bitrdi G FriendGraph X V N u X Q N u N WWalksN G u 0 = X lastS u X
31 wwlknbp1 u N WWalksN G N 0 u Word Vtx G u = N + 1
32 3simpc N 0 u Word Vtx G u = N + 1 u Word Vtx G u = N + 1
33 31 32 syl u N WWalksN G u Word Vtx G u = N + 1
34 1 wrdeqi Word V = Word Vtx G
35 34 eleq2i u Word V u Word Vtx G
36 35 anbi1i u Word V u = N + 1 u Word Vtx G u = N + 1
37 33 36 sylibr u N WWalksN G u Word V u = N + 1
38 simpll u Word V u = N + 1 G FriendGraph X V N u Word V
39 nnnn0 N N 0
40 2nn 2
41 40 a1i N 2
42 41 nnzd N 2
43 nn0pzuz N 0 2 N + 2 2
44 39 42 43 syl2anc N N + 2 2
45 3 numclwwlkovh X V N + 2 2 X H N + 2 = w N + 2 ClWWalksN G | w 0 = X w N + 2 - 2 w 0
46 44 45 sylan2 X V N X H N + 2 = w N + 2 ClWWalksN G | w 0 = X w N + 2 - 2 w 0
47 46 eleq2d X V N x X H N + 2 x w N + 2 ClWWalksN G | w 0 = X w N + 2 - 2 w 0
48 fveq1 w = x w 0 = x 0
49 48 eqeq1d w = x w 0 = X x 0 = X
50 fveq1 w = x w N + 2 - 2 = x N + 2 - 2
51 50 48 neeq12d w = x w N + 2 - 2 w 0 x N + 2 - 2 x 0
52 49 51 anbi12d w = x w 0 = X w N + 2 - 2 w 0 x 0 = X x N + 2 - 2 x 0
53 52 elrab x w N + 2 ClWWalksN G | w 0 = X w N + 2 - 2 w 0 x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0
54 47 53 bitrdi X V N x X H N + 2 x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0
55 54 3adant1 G FriendGraph X V N x X H N + 2 x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0
56 55 adantl u Word V u = N + 1 G FriendGraph X V N x X H N + 2 x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0
57 1 clwwlknbp x N + 2 ClWWalksN G x Word V x = N + 2
58 lencl u Word V u 0
59 simprr u 0 u = N + 1 N x = N + 2 x Word V x Word V
60 df-2 2 = 1 + 1
61 60 a1i N 2 = 1 + 1
62 61 oveq2d N N + 2 = N + 1 + 1
63 nncn N N
64 1cnd N 1
65 63 64 64 addassd N N + 1 + 1 = N + 1 + 1
66 62 65 eqtr4d N N + 2 = N + 1 + 1
67 66 adantl u 0 u = N + 1 N N + 2 = N + 1 + 1
68 67 eqeq2d u 0 u = N + 1 N x = N + 2 x = N + 1 + 1
69 68 biimpcd x = N + 2 u 0 u = N + 1 N x = N + 1 + 1
70 69 adantr x = N + 2 x Word V u 0 u = N + 1 N x = N + 1 + 1
71 70 impcom u 0 u = N + 1 N x = N + 2 x Word V x = N + 1 + 1
72 oveq1 u = N + 1 u + 1 = N + 1 + 1
73 72 ad3antlr u 0 u = N + 1 N x = N + 2 x Word V u + 1 = N + 1 + 1
74 71 73 eqtr4d u 0 u = N + 1 N x = N + 2 x Word V x = u + 1
75 59 74 jca u 0 u = N + 1 N x = N + 2 x Word V x Word V x = u + 1
76 75 exp31 u 0 u = N + 1 N x = N + 2 x Word V x Word V x = u + 1
77 58 76 sylan u Word V u = N + 1 N x = N + 2 x Word V x Word V x = u + 1
78 77 com12 N u Word V u = N + 1 x = N + 2 x Word V x Word V x = u + 1
79 78 3ad2ant3 G FriendGraph X V N u Word V u = N + 1 x = N + 2 x Word V x Word V x = u + 1
80 79 impcom u Word V u = N + 1 G FriendGraph X V N x = N + 2 x Word V x Word V x = u + 1
81 80 com12 x = N + 2 x Word V u Word V u = N + 1 G FriendGraph X V N x Word V x = u + 1
82 81 ancoms x Word V x = N + 2 u Word V u = N + 1 G FriendGraph X V N x Word V x = u + 1
83 57 82 syl x N + 2 ClWWalksN G u Word V u = N + 1 G FriendGraph X V N x Word V x = u + 1
84 83 adantr x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0 u Word V u = N + 1 G FriendGraph X V N x Word V x = u + 1
85 84 com12 u Word V u = N + 1 G FriendGraph X V N x N + 2 ClWWalksN G x 0 = X x N + 2 - 2 x 0 x Word V x = u + 1
86 56 85 sylbid u Word V u = N + 1 G FriendGraph X V N x X H N + 2 x Word V x = u + 1
87 86 ralrimiv u Word V u = N + 1 G FriendGraph X V N x X H N + 2 x Word V x = u + 1
88 38 87 jca u Word V u = N + 1 G FriendGraph X V N u Word V x X H N + 2 x Word V x = u + 1
89 88 ex u Word V u = N + 1 G FriendGraph X V N u Word V x X H N + 2 x Word V x = u + 1
90 37 89 syl u N WWalksN G G FriendGraph X V N u Word V x X H N + 2 x Word V x = u + 1
91 90 adantr u N WWalksN G u 0 = X lastS u X G FriendGraph X V N u Word V x X H N + 2 x Word V x = u + 1
92 91 imp u N WWalksN G u 0 = X lastS u X G FriendGraph X V N u Word V x X H N + 2 x Word V x = u + 1
93 nfcv _ v X
94 nfmpo1 _ v v V , n 2 w v ClWWalksNOn G n | w n 2 v
95 3 94 nfcxfr _ v H
96 nfcv _ v N + 2
97 93 95 96 nfov _ v X H N + 2
98 97 reuccatpfxs1 u Word V x X H N + 2 x Word V x = u + 1 ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix u
99 92 98 syl u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix u
100 99 imp u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix u
101 31 simp3d u N WWalksN G u = N + 1
102 101 eqcomd u N WWalksN G N + 1 = u
103 102 ad4antr u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 x X H N + 2 N + 1 = u
104 103 oveq2d u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 x X H N + 2 x prefix N + 1 = x prefix u
105 104 eqeq2d u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 x X H N + 2 u = x prefix N + 1 u = x prefix u
106 105 reubidva u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1 ∃! x X H N + 2 u = x prefix u
107 100 106 mpbird u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1
108 107 exp31 u N WWalksN G u 0 = X lastS u X G FriendGraph X V N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1
109 108 com12 G FriendGraph X V N u N WWalksN G u 0 = X lastS u X ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1
110 30 109 sylbid G FriendGraph X V N u X Q N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1
111 110 imp G FriendGraph X V N u X Q N ∃! v V u ++ ⟨“ v ”⟩ X H N + 2 ∃! x X H N + 2 u = x prefix N + 1
112 20 111 mpd G FriendGraph X V N u X Q N ∃! x X H N + 2 u = x prefix N + 1
113 112 ralrimiva G FriendGraph X V N u X Q N ∃! x X H N + 2 u = x prefix N + 1
114 4 f1ompt R : X H N + 2 1-1 onto X Q N x X H N + 2 x prefix N + 1 X Q N u X Q N ∃! x X H N + 2 u = x prefix N + 1
115 18 113 114 sylanbrc G FriendGraph X V N R : X H N + 2 1-1 onto X Q N