Metamath Proof Explorer


Theorem clwwlkext2edg

Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v 𝑉 = ( Vtx ‘ 𝐺 )
clwwlkext2edg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion clwwlkext2edg ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlkext2edg.e 𝐸 = ( Edg ‘ 𝐺 )
3 clwwlknnn ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )
4 1 2 isclwwlknx ( 𝑁 ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ) )
5 ige2m2fzo ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
6 5 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
7 6 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
8 oveq1 ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( 𝑁 − 1 ) )
9 8 oveq2d ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
10 9 eleq2d ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
11 10 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
12 7 11 mpbird ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) )
13 fveq2 ( 𝑖 = ( 𝑁 − 2 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) )
14 fvoveq1 ( 𝑖 = ( 𝑁 − 2 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) )
15 13 14 preq12d ( 𝑖 = ( 𝑁 − 2 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } )
16 15 eleq1d ( 𝑖 = ( 𝑁 − 2 ) → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
17 16 rspcv ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
18 12 17 syl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ) )
19 wrdlenccats1lenm1 ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑊 ) )
20 19 eqcomd ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) )
21 20 adantr ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) )
22 21 8 sylan9eq ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) )
23 22 ex ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) )
24 23 3adant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) )
25 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℂ )
26 1cnd ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 ∈ ℂ )
27 25 26 26 subsub4d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) )
28 1p1e2 ( 1 + 1 ) = 2
29 28 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 1 + 1 ) = 2 )
30 29 oveq2d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − ( 1 + 1 ) ) = ( 𝑁 − 2 ) )
31 27 30 eqtr2d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
32 31 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑁 − 2 ) = ( ( 𝑁 − 1 ) − 1 ) )
33 oveq1 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 − 1 ) − 1 ) )
34 33 eqcomd ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( 𝑁 − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
35 32 34 sylan9eq ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
36 35 ex ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
37 24 36 syld ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
38 37 imp ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑁 − 2 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
39 38 fveq2d ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
40 simpl1 ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ∈ Word 𝑉 )
41 s1cl ( 𝑍𝑉 → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
42 41 3ad2ant2 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
43 42 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 )
44 eluz2 ( 𝑁 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
45 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
46 1red ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 ∈ ℝ )
47 2re 2 ∈ ℝ
48 47 a1i ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 2 ∈ ℝ )
49 simpl ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
50 1lt2 1 < 2
51 50 a1i ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 < 2 )
52 simpr ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 2 ≤ 𝑁 )
53 46 48 49 51 52 ltletrd ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 < 𝑁 )
54 1red ( 𝑁 ∈ ℝ → 1 ∈ ℝ )
55 id ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
56 54 55 posdifd ( 𝑁 ∈ ℝ → ( 1 < 𝑁 ↔ 0 < ( 𝑁 − 1 ) ) )
57 56 adantr ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( 1 < 𝑁 ↔ 0 < ( 𝑁 − 1 ) ) )
58 53 57 mpbid ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 0 < ( 𝑁 − 1 ) )
59 58 ex ( 𝑁 ∈ ℝ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) )
60 45 59 syl ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) )
61 60 a1i ( 2 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → 0 < ( 𝑁 − 1 ) ) ) )
62 61 3imp ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → 0 < ( 𝑁 − 1 ) )
63 44 62 sylbi ( 𝑁 ∈ ( ℤ ‘ 2 ) → 0 < ( 𝑁 − 1 ) )
64 63 ad2antlr ( ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( 𝑁 − 1 ) )
65 breq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
66 65 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
67 64 66 mpbird ( ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
68 hashneq0 ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
69 68 adantr ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
70 69 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
71 67 70 mpbid ( ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ≠ ∅ )
72 71 3adantl2 ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 𝑊 ≠ ∅ )
73 40 43 72 3jca ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) )
74 73 ex ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) ) )
75 24 74 syld ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) ) )
76 75 imp ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) )
77 ccatval1lsw ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
78 76 77 syl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
79 39 78 eqtrd ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = ( lastS ‘ 𝑊 ) )
80 2m1e1 ( 2 − 1 ) = 1
81 80 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 2 − 1 ) = 1 )
82 81 eqcomd ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 = ( 2 − 1 ) )
83 82 oveq2d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 1 ) = ( 𝑁 − ( 2 − 1 ) ) )
84 2cnd ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ∈ ℂ )
85 25 84 26 subsubd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) )
86 83 85 eqtr2d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) )
87 86 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) )
88 eqeq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ↔ ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) ) )
89 87 88 syl5ibrcom ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) )
90 24 89 syld ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) )
91 90 imp ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑁 − 2 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
92 91 fveq2d ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) )
93 id ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) )
94 93 3adant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) )
95 94 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) )
96 ccatws1ls ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
97 95 96 syl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑍 )
98 92 97 eqtrd ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑍 )
99 79 98 preq12d ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } = { ( lastS ‘ 𝑊 ) , 𝑍 } )
100 99 eleq1d ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑁 − 2 ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) )
101 18 100 sylibd ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) )
102 101 ex ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
103 102 com13 ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
104 103 3ad2ant2 ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ) ) )
105 104 imp31 ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 )
106 94 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) )
107 lswccats1 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉 ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
108 106 107 syl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑍 )
109 63 3ad2ant3 ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → 0 < ( 𝑁 − 1 ) )
110 109 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( 𝑁 − 1 ) )
111 65 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 − 1 ) ) )
112 110 111 mpbird ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
113 ccatfv0 ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
114 40 43 112 113 syl3anc ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
115 108 114 preq12d ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
116 115 ex ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 1 ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } ) )
117 24 116 syld ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } ) )
118 117 impcom ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } = { 𝑍 , ( 𝑊 ‘ 0 ) } )
119 118 eleq1d ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ↔ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
120 119 biimpcd ( { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 → ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
121 120 3ad2ant3 ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) → ( ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
122 121 impl ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
123 105 122 jca ( ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) ∧ ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
124 123 ex ( ( ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) , ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ‘ 0 ) } ∈ 𝐸 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = 𝑁 ) → ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
125 4 124 syl6bi ( 𝑁 ∈ ℕ → ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) )
126 3 125 mpcom ( ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) )
127 126 impcom ( ( ( 𝑊 ∈ Word 𝑉𝑍𝑉𝑁 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( { ( lastS ‘ 𝑊 ) , 𝑍 } ∈ 𝐸 ∧ { 𝑍 , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )