| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1w 2823 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ (𝑋𝐻(𝑁 + 2)))) | 
| 2 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) | 
| 3 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1))) | 
| 4 | 2, 3 | eqeq12d 2752 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) = (𝑦 prefix (𝑁 + 1)) ↔ (𝑅‘𝑥) = (𝑥 prefix (𝑁 + 1)))) | 
| 5 | 1, 4 | imbi12d 344 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 prefix (𝑁 + 1))) ↔ (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 prefix (𝑁 + 1))))) | 
| 6 | 5 | imbi2d 340 | . . . . . . 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))) | 
| 11 | 7, 8, 9, 10 | numclwlk2lem2fv 30398 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 prefix (𝑁 + 1)))) | 
| 12 | 6, 11 | chvarvv 1997 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 prefix (𝑁 + 1)))) | 
| 13 | 12 | 3adant1 1130 | . . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 prefix (𝑁 + 1)))) | 
| 14 | 13 | imp 406 | . . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) = (𝑥 prefix (𝑁 + 1))) | 
| 15 | 7, 8, 9, 10 | numclwlk2lem2f 30397 | . . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁)) | 
| 16 | 15 | ffvelcdmda 7103 | . . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) ∈ (𝑋𝑄𝑁)) | 
| 17 | 14, 16 | eqeltrrd 2841 | . . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁)) | 
| 18 | 17 | ralrimiva 3145 | . 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁)) | 
| 19 | 7, 8, 9 | numclwwlk2lem1 30396 | . . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) | 
| 20 | 19 | imp 406 | . . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) | 
| 21 | 7, 8 | numclwwlkovq 30394 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}) | 
| 22 | 21 | eleq2d 2826 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})) | 
| 23 | 22 | 3adant1 1130 | . . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})) | 
| 24 |  | fveq1 6904 | . . . . . . . . . 10
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) | 
| 25 | 24 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋)) | 
| 26 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑢 → (lastS‘𝑤) = (lastS‘𝑢)) | 
| 27 | 26 | neeq1d 2999 | . . . . . . . . 9
⊢ (𝑤 = 𝑢 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑢) ≠ 𝑋)) | 
| 28 | 25, 27 | anbi12d 632 | . . . . . . . 8
⊢ (𝑤 = 𝑢 → (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) ↔ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋))) | 
| 29 | 28 | elrab 3691 | . . . . . . 7
⊢ (𝑢 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} ↔ (𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋))) | 
| 30 | 23, 29 | bitrdi 287 | . . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ (𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)))) | 
| 31 |  | wwlknbp1 29865 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1))) | 
| 32 |  | 3simpc 1150 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑢 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑢) = (𝑁 + 1)) → (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1))) | 
| 33 | 31, 32 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1))) | 
| 34 | 7 | wrdeqi 14576 | . . . . . . . . . . . . . . . . 17
⊢ Word
𝑉 = Word (Vtx‘𝐺) | 
| 35 | 34 | eleq2i 2832 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ Word 𝑉 ↔ 𝑢 ∈ Word (Vtx‘𝐺)) | 
| 36 | 35 | anbi1i 624 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ↔ (𝑢 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑢) = (𝑁 + 1))) | 
| 37 | 33, 36 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1))) | 
| 38 |  | simpll 766 | . . . . . . . . . . . . . . . 16
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑢 ∈ Word 𝑉) | 
| 39 |  | nnnn0 12535 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 40 |  | 2nn 12340 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ | 
| 41 | 40 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ) | 
| 42 | 41 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 2 ∈
ℤ) | 
| 43 |  | nn0pzuz 12948 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℤ) → (𝑁 + 2) ∈
(ℤ≥‘2)) | 
| 44 | 39, 42, 43 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
(ℤ≥‘2)) | 
| 45 | 9 | numclwwlkovh 30393 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2)) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) | 
| 46 | 44, 45 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) | 
| 47 | 46 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) | 
| 48 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) | 
| 49 | 48 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → ((𝑤‘0) = 𝑋 ↔ (𝑥‘0) = 𝑋)) | 
| 50 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → (𝑤‘((𝑁 + 2) − 2)) = (𝑥‘((𝑁 + 2) − 2))) | 
| 51 | 50, 48 | neeq12d 3001 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) | 
| 52 | 49, 51 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑥 → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) | 
| 53 | 52 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) | 
| 54 | 47, 53 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) | 
| 55 | 54 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) | 
| 57 | 7 | clwwlknbp 30055 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = (𝑁 + 2))) | 
| 58 |  | lencl 14572 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 ∈ Word 𝑉 → (♯‘𝑢) ∈
ℕ0) | 
| 59 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((♯‘𝑢) ∈ ℕ0 ∧
(♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → 𝑥 ∈ Word 𝑉) | 
| 60 |  | df-2 12330 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 2 = (1 +
1) | 
| 61 | 60 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ → 2 = (1 +
1)) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = (𝑁 + (1 + 1))) | 
| 63 |  | nncn 12275 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 64 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) | 
| 65 | 63, 64, 64 | addassd 11284 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1))) | 
| 66 | 62, 65 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = ((𝑁 + 1) + 1)) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((♯‘𝑢)
∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) = ((𝑁 + 1) + 1)) | 
| 68 | 67 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((♯‘𝑢)
∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) →
((♯‘𝑥) = (𝑁 + 2) ↔
(♯‘𝑥) = ((𝑁 + 1) + 1))) | 
| 69 | 68 | biimpcd 249 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝑥) =
(𝑁 + 2) →
((((♯‘𝑢) ∈
ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (♯‘𝑥) = ((𝑁 + 1) + 1))) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((♯‘𝑥)
= (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((((♯‘𝑢) ∈ ℕ0
∧ (♯‘𝑢) =
(𝑁 + 1)) ∧ 𝑁 ∈ ℕ) →
(♯‘𝑥) = ((𝑁 + 1) + 1))) | 
| 71 | 70 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((♯‘𝑢) ∈ ℕ0 ∧
(♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (♯‘𝑥) = ((𝑁 + 1) + 1)) | 
| 72 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑢) =
(𝑁 + 1) →
((♯‘𝑢) + 1) =
((𝑁 + 1) +
1)) | 
| 73 | 72 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((♯‘𝑢) ∈ ℕ0 ∧
(♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((♯‘𝑢) + 1) = ((𝑁 + 1) + 1)) | 
| 74 | 71, 73 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((♯‘𝑢) ∈ ℕ0 ∧
(♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (♯‘𝑥) = ((♯‘𝑢) + 1)) | 
| 75 | 59, 74 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((♯‘𝑢) ∈ ℕ0 ∧
(♯‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))) | 
| 76 | 75 | exp31 419 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑢)
∈ ℕ0 ∧ (♯‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ →
(((♯‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 77 | 58, 76 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ →
(((♯‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 78 | 77 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 79 | 78 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → (((♯‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 80 | 79 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) →
(((♯‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 81 | 80 | com12 32 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑥)
= (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 82 | 81 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = (𝑁 + 2)) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 83 | 57, 82 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 85 | 84 | com12 32 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝑥 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 86 | 56, 85 | sylbid 240 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 87 | 86 | ralrimiv 3144 | . . . . . . . . . . . . . . . 16
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))) | 
| 88 | 38, 87 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 89 | 88 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ Word 𝑉 ∧ (♯‘𝑢) = (𝑁 + 1)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 90 | 37, 89 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))))) | 
| 92 | 91 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1)))) | 
| 93 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣𝑋 | 
| 94 |  | nfmpo1 7514 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑣(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣}) | 
| 95 | 9, 94 | nfcxfr 2902 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣𝐻 | 
| 96 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣(𝑁 + 2) | 
| 97 | 93, 95, 96 | nfov 7462 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣(𝑋𝐻(𝑁 + 2)) | 
| 98 | 97 | reuccatpfxs1 14786 | . . . . . . . . . . 11
⊢ ((𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑢) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢)))) | 
| 99 | 92, 98 | syl 17 | . . . . . . . . . 10
⊢ (((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢)))) | 
| 100 | 99 | imp 406 | . . . . . . . . 9
⊢ ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢))) | 
| 101 | 31 | simp3d 1144 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → (♯‘𝑢) = (𝑁 + 1)) | 
| 102 | 101 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ (𝑁 WWalksN 𝐺) → (𝑁 + 1) = (♯‘𝑢)) | 
| 103 | 102 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑁 + 1) = (♯‘𝑢)) | 
| 104 | 103 | oveq2d 7448 | . . . . . . . . . . 11
⊢
(((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (♯‘𝑢))) | 
| 105 | 104 | eqeq2d 2747 | . . . . . . . . . 10
⊢
(((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑢 = (𝑥 prefix (𝑁 + 1)) ↔ 𝑢 = (𝑥 prefix (♯‘𝑢)))) | 
| 106 | 105 | reubidva 3395 | . . . . . . . . 9
⊢ ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → (∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)) ↔ ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (♯‘𝑢)))) | 
| 107 | 100, 106 | mpbird 257 | . . . . . . . 8
⊢ ((((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))) | 
| 108 | 107 | exp31 419 | . . . . . . 7
⊢ ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))))) | 
| 109 | 108 | com12 32 | . . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ (lastS‘𝑢) ≠ 𝑋)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))))) | 
| 110 | 30, 109 | sylbid 240 | . . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))))) | 
| 111 | 110 | imp 406 | . . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))) | 
| 112 | 20, 111 | mpd 15 | . . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))) | 
| 113 | 112 | ralrimiva 3145 | . 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1))) | 
| 114 | 10 | f1ompt 7130 | . 2
⊢ (𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁) ↔ (∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 prefix (𝑁 + 1)) ∈ (𝑋𝑄𝑁) ∧ ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 prefix (𝑁 + 1)))) | 
| 115 | 18, 113, 114 | sylanbrc 583 | 1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁)) |