MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  numclwlk2lem2f1o Structured version   Visualization version   GIF version

Theorem numclwlk2lem2f1o 27850
Description: 𝑅 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.)
Hypotheses
Ref Expression
numclwwlk.v 𝑉 = (Vtx‘𝐺)
numclwwlk.q 𝑄 = (𝑣𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
numclwwlk.h 𝐻 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})
numclwwlk.r 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 prefix (𝑁 + 1)))
Assertion
Ref Expression
numclwlk2lem2f1o ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁))
Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑛,𝑉,𝑣   𝑛,𝑋,𝑣,𝑤   𝑤,𝑉   𝑥,𝐺,𝑤   𝑥,𝐻   𝑥,𝑁   𝑥,𝑄   𝑥,𝑉   𝑥,𝑋,𝑣
Allowed substitution hints:   𝑄(𝑤,𝑣,𝑛)   𝑅(𝑥,𝑤,𝑣,𝑛)   𝐻(𝑤,𝑣,𝑛)

Proof of Theorem numclwlk2lem2f1o
Dummy variables 𝑦 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1w 2865 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))))
2 fveq2 6538 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑅𝑦) = (𝑅𝑥))
3 oveq1 7023 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1)))
42, 3eqeq12d 2810 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑅𝑦) = (𝑦 prefix (𝑁 + 1)) ↔ (𝑅𝑥) = (𝑥 prefix (𝑁 + 1))))
51, 4imbi12d 346 . . . . . . . 8 (𝑦 = 𝑥 → ((𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑦) = (𝑦 prefix (𝑁 + 1))) ↔ (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑥) = (𝑥 prefix (𝑁 + 1)))))
65imbi2d 342 . . . . . . 7 (𝑦 = 𝑥 → (((𝑋𝑉𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑦) = (𝑦 prefix (𝑁 + 1)))) ↔ ((𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑥) = (𝑥 prefix (𝑁 + 1))))))
7 numclwwlk.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
8 numclwwlk.q . . . . . . . 8 𝑄 = (𝑣𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
9 numclwwlk.h . . . . . . . 8 𝐻 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})
10 numclwwlk.r . . . . . . . 8 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 prefix (𝑁 + 1)))
117, 8, 9, 10numclwlk2lem2fv 27849 . . . . . . 7 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑦) = (𝑦 prefix (𝑁 + 1))))
126, 11chvarv 2370 . . . . . 6 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑥) = (𝑥 prefix (𝑁 + 1))))
13123adant1 1123 . . . . 5 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅𝑥) = (𝑥 prefix (𝑁 + 1))))
1413imp 407 . . . 4 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅𝑥) = (𝑥 prefix (𝑁 + 1)))
157, 8, 9, 10numclwlk2lem2f 27848 . . . . 5 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁))
1615ffvelrnda 6716 . . . 4 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅𝑥) ∈ (𝑋𝑄𝑁))
1714, 16eqeltrrd 2884 . . 3 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁))
1817ralrimiva 3149 . 2 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁))
197, 8, 9numclwwlk2lem1 27847 . . . . 5 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
2019imp 407 . . . 4 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)))
217, 8numclwwlkovq 27845 . . . . . . . . 9 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})
2221eleq2d 2868 . . . . . . . 8 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}))
23223adant1 1123 . . . . . . 7 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}))
24 fveq1 6537 . . . . . . . . . 10 (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0))
2524eqeq1d 2797 . . . . . . . . 9 (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋))
26 fveq2 6538 . . . . . . . . . 10 (𝑤 = 𝑢 → (lastS‘𝑤) = (lastS‘𝑢))
2726neeq1d 3043 . . . . . . . . 9 (𝑤 = 𝑢 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑢) ≠ 𝑋))
2825, 27anbi12d 630 . . . . . . . 8 (𝑤 = 𝑢 → (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) ↔ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)))
2928elrab 3618 . . . . . . 7 (𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} ↔ (𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)))
3023, 29syl6bb 288 . . . . . 6 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ (𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋))))
31 wwlknbp1 27309 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1)))
32 3simpc 1143 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1)) → (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1)))
3331, 32syl 17 . . . . . . . . . . . . . . 15 (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1)))
347wrdeqi 13733 . . . . . . . . . . . . . . . . 17 Word 𝑉 = Word (Vtx‘𝐺)
3534eleq2i 2874 . . . . . . . . . . . . . . . 16 (𝑢 ∈ Word 𝑉𝑢 ∈ Word (Vtx‘𝐺))
3635anbi1i 623 . . . . . . . . . . . . . . 15 ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ↔ (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1)))
3733, 36sylibr 235 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)))
38 simpll 763 . . . . . . . . . . . . . . . 16 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → 𝑢 ∈ Word 𝑉)
39 nnnn0 11752 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
40 2nn 11558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℕ
4140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 2 ∈ ℕ)
4241nnzd 11935 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 2 ∈ ℤ)
43 nn0pzuz 12154 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ) → (𝑁 + 2) ∈ (ℤ‘2))
4439, 42, 43syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ (ℤ‘2))
459numclwwlkovh 27844 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑉 ∧ (𝑁 + 2) ∈ (ℤ‘2)) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
4644, 45sylan2 592 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
4746eleq2d 2868 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}))
48 fveq1 6537 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
4948eqeq1d 2797 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑥 → ((𝑤‘0) = 𝑋 ↔ (𝑥‘0) = 𝑋))
50 fveq1 6537 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑤‘((𝑁 + 2) − 2)) = (𝑥‘((𝑁 + 2) − 2)))
5150, 48neeq12d 3045 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑥 → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))
5249, 51anbi12d 630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑥 → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))
5352elrab 3618 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))
5447, 53syl6bb 288 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
55543adant1 1123 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
5655adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
577clwwlknbp 27500 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = (𝑁 + 2)))
58 lencl 13729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ Word 𝑉 → (♯‘𝑢) ∈ ℕ0)
59 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → 𝑥 ∈ Word 𝑉)
60 df-2 11548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2 = (1 + 1)
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑁 ∈ ℕ → 2 = (1 + 1))
6261oveq2d 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ ℕ → (𝑁 + 2) = (𝑁 + (1 + 1)))
63 nncn 11494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
64 1cnd 10482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑁 ∈ ℕ → 1 ∈ ℂ)
6563, 64, 64addassd 10509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
6662, 65eqtr4d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ ℕ → (𝑁 + 2) = ((𝑁 + 1) + 1))
6766adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) = ((𝑁 + 1) + 1))
6867eqeq2d 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((♯‘𝑥) = (𝑁 + 2) ↔ (♯‘𝑥) = ((𝑁 + 1) + 1)))
6968biimpcd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((♯‘𝑥) = (𝑁 + 2) → ((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (♯‘𝑥) = ((𝑁 + 1) + 1)))
7069adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (♯‘𝑥) = ((𝑁 + 1) + 1)))
7170impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (♯‘𝑥) = ((𝑁 + 1) + 1))
72 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝑢) = (𝑁 + 1) → ((♯‘𝑢) + 1) = ((𝑁 + 1) + 1))
7372ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((♯‘𝑢) + 1) = ((𝑁 + 1) + 1))
7471, 73eqtr4d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (♯‘𝑥) = ((♯‘𝑢) + 1))
7559, 74jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))
7675exp31 420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑢) ∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
7758, 76sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
7877com12 32 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
79783ad2ant3 1128 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
8079impcom 408 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8180com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8281ancoms 459 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = (𝑁 + 2)) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8357, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8483adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8584com12 32 . . . . . . . . . . . . . . . . . 18 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → ((𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8656, 85sylbid 241 . . . . . . . . . . . . . . . . 17 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8786ralrimiv 3148 . . . . . . . . . . . . . . . 16 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))
8838, 87jca 512 . . . . . . . . . . . . . . 15 (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
8988ex 413 . . . . . . . . . . . . . 14 ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
9037, 89syl 17 . . . . . . . . . . . . 13 (𝑢 ∈ (𝑁 WWalksN 𝐺) → ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
9190adantr 481 . . . . . . . . . . . 12 ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))))
9291imp 407 . . . . . . . . . . 11 (((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))
93 nfcv 2949 . . . . . . . . . . . . 13 𝑣𝑋
94 nfmpo1 7092 . . . . . . . . . . . . . 14 𝑣(𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})
959, 94nfcxfr 2947 . . . . . . . . . . . . 13 𝑣𝐻
96 nfcv 2949 . . . . . . . . . . . . 13 𝑣(𝑁 + 2)
9793, 95, 96nfov 7046 . . . . . . . . . . . 12 𝑣(𝑋𝐻(𝑁 + 2))
9897reuccatpfxs1 13945 . . . . . . . . . . 11 ((𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢))))
9992, 98syl 17 . . . . . . . . . 10 (((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢))))
10099imp 407 . . . . . . . . 9 ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢)))
10131simp3d 1137 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝑁 WWalksN 𝐺) → (♯‘𝑢) = (𝑁 + 1))
102101eqcomd 2801 . . . . . . . . . . . . 13 (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑁 + 1) = (♯‘𝑢))
103102ad4antr 728 . . . . . . . . . . . 12 (((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑁 + 1) = (♯‘𝑢))
104103oveq2d 7032 . . . . . . . . . . 11 (((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (♯‘𝑢)))
105104eqeq2d 2805 . . . . . . . . . 10 (((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑢 = (𝑥 prefix (𝑁 + 1)) ↔ 𝑢 = (𝑥 prefix (♯‘𝑢))))
106105reubidva 3347 . . . . . . . . 9 ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → (∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)) ↔ ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢))))
107100, 106mpbird 258 . . . . . . . 8 ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ)) ∧ ∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))
108107exp31 420 . . . . . . 7 ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))))
109108com12 32 . . . . . 6 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))))
11030, 109sylbid 241 . . . . 5 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))))
111110imp 407 . . . 4 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → (∃!𝑣𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))))
11220, 111mpd 15 . . 3 (((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))
113112ralrimiva 3149 . 2 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))
11410f1ompt 6738 . 2 (𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁) ↔ (∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁) ∧ ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))))
11518, 113, 114sylanbrc 583 1 ((𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wcel 2081  wne 2984  wral 3105  ∃!wreu 3107  {crab 3109  cmpt 5041  1-1-ontowf1o 6224  cfv 6225  (class class class)co 7016  cmpo 7018  0cc0 10383  1c1 10384   + caddc 10386  cmin 10717  cn 11486  2c2 11540  0cn0 11745  cz 11829  cuz 12093  chash 13540  Word cword 13707  lastSclsw 13760   ++ cconcat 13768  ⟨“cs1 13793   prefix cpfx 13868  Vtxcvtx 26464   WWalksN cwwlksn 27291   ClWWalksN cclwwlkn 27489  ClWWalksNOncclwwlknon 27553   FriendGraph cfrgr 27727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-n0 11746  df-xnn0 11816  df-z 11830  df-uz 12094  df-rp 12240  df-fz 12743  df-fzo 12884  df-hash 13541  df-word 13708  df-lsw 13761  df-concat 13769  df-s1 13794  df-substr 13839  df-pfx 13869  df-wwlks 27295  df-wwlksn 27296  df-clwwlk 27447  df-clwwlkn 27490  df-clwwlknon 27554  df-frgr 27728
This theorem is referenced by:  numclwwlk2lem3  27851
  Copyright terms: Public domain W3C validator