Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ (𝑋𝐻(𝑁 + 2)))) |
2 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
3 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
4 | 2, 3 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) = (𝑦 substr 〈0, (𝑁 + 1)〉) ↔ (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
5 | 1, 4 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr 〈0, (𝑁 + 1)〉)) ↔ (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉)))) |
6 | 5 | imbi2d 329 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr 〈0, (𝑁 + 1)〉))) ↔ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉))))) |
7 | | numclwwlk.c |
. . . . . . . 8
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
8 | | numclwwlk.f |
. . . . . . . 8
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
9 | | numclwwlk.g |
. . . . . . . 8
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
10 | | numclwwlk.q |
. . . . . . . 8
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
11 | | numclwwlk.h |
. . . . . . . 8
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
12 | | numclwwlk.r |
. . . . . . . 8
⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 substr 〈0, (𝑁 + 1)〉)) |
13 | 7, 8, 9, 10, 11, 12 | numclwlk2lem2fv 26631 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr 〈0, (𝑁 + 1)〉))) |
14 | 6, 13 | chvarv 2251 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
15 | 14 | 3adant1 1072 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
16 | 15 | imp 444 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
17 | 7, 8, 9, 10, 11, 12 | numclwlk2lem2f 26630 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁)) |
18 | 17 | ffvelrnda 6267 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) ∈ (𝑋𝑄𝑁)) |
19 | 16, 18 | eqeltrrd 2689 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁)) |
20 | 19 | ralrimiva 2949 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁)) |
21 | 7, 8, 9, 10, 11 | numclwwlk2lem1 26629 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
22 | 21 | imp 444 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) |
23 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
24 | 7, 8, 9, 10 | numclwwlkovq 26626 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
25 | 23, 24 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
26 | 25 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})) |
27 | 26 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})) |
28 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
29 | 28 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋)) |
30 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → ( lastS ‘𝑤) = ( lastS ‘𝑢)) |
31 | 30 | neeq1d 2841 |
. . . . . . . . 9
⊢ (𝑤 = 𝑢 → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑢) ≠ 𝑋)) |
32 | 29, 31 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑤 = 𝑢 → (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) ↔ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋))) |
33 | 32 | elrab 3331 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} ↔ (𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋))) |
34 | 27, 33 | syl6bb 275 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ (𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)))) |
35 | | wwlknimpb 26232 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1))) |
36 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑢 ∈ Word 𝑉) |
37 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ0 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
39 | 23, 38 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℕ0) |
40 | 7, 8, 9, 10, 11 | numclwwlkovh 26628 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ0) →
(𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
41 | 39, 40 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
42 | 41 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) |
43 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
44 | 43 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → ((𝑤‘0) = 𝑋 ↔ (𝑥‘0) = 𝑋)) |
45 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑥 → (𝑤‘((𝑁 + 2) − 2)) = (𝑥‘((𝑁 + 2) − 2))) |
46 | 45, 43 | neeq12d 2843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) |
47 | 44, 46 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) |
48 | 47 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ {𝑤 ∈ (𝐶‘(𝑁 + 2)) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
50 | 7 | numclwwlkfvc 26604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 + 2) ∈ ℕ0
→ (𝐶‘(𝑁 + 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))) |
51 | 39, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (𝐶‘(𝑁 + 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2))) |
52 | 51 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (𝐶‘(𝑁 + 2)) ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝐶‘(𝑁 + 2)) ↔ 𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) |
54 | 53 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ (𝐶‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
55 | 42, 49, 54 | 3bitrd 293 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
56 | 55 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))) |
58 | | clwwlknprop 26300 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2)))) |
59 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ Word 𝑉 → (#‘𝑢) ∈
ℕ0) |
60 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → 𝑥 ∈ Word 𝑉) |
61 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 2 = (1 +
1) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℕ → 2 = (1 +
1)) |
63 | 62 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = (𝑁 + (1 + 1))) |
64 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
65 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
66 | 64, 65, 65 | addassd 9941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1))) |
67 | 63, 66 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = ((𝑁 + 1) + 1)) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) = ((𝑁 + 1) + 1)) |
69 | 68 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((#‘𝑥) = (𝑁 + 2) ↔ (#‘𝑥) = ((𝑁 + 1) + 1))) |
70 | 69 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝑥) =
(𝑁 + 2) →
((((#‘𝑢) ∈
ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘𝑥) = ((𝑁 + 1) + 1))) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((((#‘𝑢) ∈ ℕ0 ∧
(#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘𝑥) = ((𝑁 + 1) + 1))) |
72 | 71 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (#‘𝑥) = ((𝑁 + 1) + 1)) |
73 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝑢) =
(𝑁 + 1) →
((#‘𝑢) + 1) = ((𝑁 + 1) + 1)) |
74 | 73 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((#‘𝑢) + 1) = ((𝑁 + 1) + 1)) |
75 | 72, 74 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (#‘𝑥) = ((#‘𝑢) + 1)) |
76 | 60, 75 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((#‘𝑢)
∈ ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))) |
77 | 76 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝑢) ∈
ℕ0 ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
78 | 59, 77 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
79 | 78 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
80 | 79 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
81 | 80 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
82 | 81 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
83 | 82 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑥) =
(𝑁 + 2) → (𝑥 ∈ Word 𝑉 → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 + 2) ∈ ℕ0
∧ (#‘𝑥) = (𝑁 + 2)) → (𝑥 ∈ Word 𝑉 → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
85 | 84 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
86 | 85 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑥 ∈ Word 𝑉 ∧ ((𝑁 + 2) ∈ ℕ0 ∧
(#‘𝑥) = (𝑁 + 2))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
87 | 58, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
90 | 57, 89 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
91 | 90 | ralrimiv 2948 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))) |
92 | 36, 91 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
93 | 92 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
94 | 35, 93 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))) |
96 | 95 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))) |
97 | | reuccats1 13332 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (#‘𝑢)〉))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (#‘𝑢)〉))) |
99 | 98 | imp 444 |
. . . . . . . . 9
⊢ ((((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (#‘𝑢)〉)) |
100 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (#‘𝑢) = (𝑁 + 1)) |
101 | 100 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 + 1) = (#‘𝑢)) |
102 | 35, 101 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑁 + 1) = (#‘𝑢)) |
103 | 102 | ad4antr 764 |
. . . . . . . . . . . . 13
⊢
(((((𝑢 ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑁 + 1) = (#‘𝑢)) |
104 | 103 | opeq2d 4347 |
. . . . . . . . . . . 12
⊢
(((((𝑢 ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → 〈0, (𝑁 + 1)〉 = 〈0, (#‘𝑢)〉) |
105 | 104 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
(((((𝑢 ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (#‘𝑢)〉)) |
106 | 105 | eqeq2d 2620 |
. . . . . . . . . 10
⊢
(((((𝑢 ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉) ↔ 𝑢 = (𝑥 substr 〈0, (#‘𝑢)〉))) |
107 | 106 | reubidva 3102 |
. . . . . . . . 9
⊢ ((((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → (∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉) ↔ ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (#‘𝑢)〉))) |
108 | 99, 107 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
109 | 108 | exp31 628 |
. . . . . . 7
⊢ ((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)))) |
110 | 109 | com12 32 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)))) |
111 | 34, 110 | sylbid 229 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)))) |
112 | 111 | imp 444 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
113 | 22, 112 | mpd 15 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
114 | 113 | ralrimiva 2949 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
115 | 12 | f1ompt 6290 |
. 2
⊢ (𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁) ↔ (∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 substr 〈0, (𝑁 + 1)〉) ∈ (𝑋𝑄𝑁) ∧ ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
116 | 20, 114, 115 | sylanbrc 695 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁)) |