This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlksnextfun

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
wwlksnextbij0.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
wwlksnextbij0.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
Assertion wwlksnextfun ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlksnextbij0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextbij0.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
4 wwlksnextbij0.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
5 wwlksnextbij0.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
6 fveqeq2 ⊢ ( 𝑤 = 𝑡 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) )
7 oveq1 ⊢ ( 𝑤 = 𝑡 → ( 𝑤 prefix ( 𝑁 + 1 ) ) = ( 𝑡 prefix ( 𝑁 + 1 ) ) )
8 7 eqeq1d ⊢ ( 𝑤 = 𝑡 → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
9 fveq2 ⊢ ( 𝑤 = 𝑡 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑡 ) )
10 9 preq2d ⊢ ( 𝑤 = 𝑡 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } )
11 10 eleq1d ⊢ ( 𝑤 = 𝑡 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
12 6 8 11 3anbi123d ⊢ ( 𝑤 = 𝑡 → ( ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) )
13 12 3 elrab2 ⊢ ( 𝑡 ∈ 𝐷 ↔ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) )
14 simpll ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 𝑡 ∈ Word 𝑉 )
15 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
18 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
19 2pos ⊢ 0 < 2
20 19 a1i ⊢ ( 𝑁 ∈ ℕ0 → 0 < 2 )
21 15 17 18 20 addgegt0d ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 2 ) )
22 21 ad2antlr ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 0 < ( 𝑁 + 2 ) )
23 breq2 ⊢ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) → ( 0 < ( ♯ ‘ 𝑡 ) ↔ 0 < ( 𝑁 + 2 ) ) )
24 23 adantl ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → ( 0 < ( ♯ ‘ 𝑡 ) ↔ 0 < ( 𝑁 + 2 ) ) )
25 22 24 mpbird ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 0 < ( ♯ ‘ 𝑡 ) )
26 hashgt0n0 ⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑡 ) ) → 𝑡 ≠ ∅ )
27 14 25 26 syl2anc ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 𝑡 ≠ ∅ )
28 14 27 jca ⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) )
29 28 expcom ⊢ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) → ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
30 29 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) → ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
31 30 expd ⊢ ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) → ( 𝑡 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) ) )
32 31 impcom ⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
33 32 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) )
34 lswcl ⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) → ( lastS ‘ 𝑡 ) ∈ 𝑉 )
35 33 34 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( lastS ‘ 𝑡 ) ∈ 𝑉 )
36 simprr3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 )
37 35 36 jca ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
38 13 37 sylan2b ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑡 ∈ 𝐷 ) → ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
39 preq2 ⊢ ( 𝑛 = ( lastS ‘ 𝑡 ) → { ( lastS ‘ 𝑊 ) , 𝑛 } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } )
40 39 eleq1d ⊢ ( 𝑛 = ( lastS ‘ 𝑡 ) → ( { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
41 40 4 elrab2 ⊢ ( ( lastS ‘ 𝑡 ) ∈ 𝑅 ↔ ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
42 38 41 sylibr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑡 ∈ 𝐷 ) → ( lastS ‘ 𝑡 ) ∈ 𝑅 )
43 42 5 fmptd ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )