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

Metamath Proof Explorer

Theorem ewlkle

Description: An s-walk of edges is also a t-walk of edges if t <_ s . (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion ewlkle ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2 1 ewlkprop ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
3 simpl2 ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
4 xnn0xr ⊢ ( 𝑇 ∈ ℕ0* → 𝑇 ∈ ℝ* )
5 4 adantl ⊢ ( ( 𝑆 ∈ ℕ0* ∧ 𝑇 ∈ ℕ0* ) → 𝑇 ∈ ℝ* )
6 xnn0xr ⊢ ( 𝑆 ∈ ℕ0* → 𝑆 ∈ ℝ* )
7 6 adantr ⊢ ( ( 𝑆 ∈ ℕ0* ∧ 𝑇 ∈ ℕ0* ) → 𝑆 ∈ ℝ* )
8 fvex ⊢ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∈ V
9 8 inex1 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V
10 hashxrcl ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* )
11 9 10 mp1i ⊢ ( ( 𝑆 ∈ ℕ0* ∧ 𝑇 ∈ ℕ0* ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* )
12 xrletr ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ* ) → ( ( 𝑇 ≤ 𝑆 ∧ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
13 5 7 11 12 syl3anc ⊢ ( ( 𝑆 ∈ ℕ0* ∧ 𝑇 ∈ ℕ0* ) → ( ( 𝑇 ≤ 𝑆 ∧ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
14 13 exp4b ⊢ ( 𝑆 ∈ ℕ0* → ( 𝑇 ∈ ℕ0* → ( 𝑇 ≤ 𝑆 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
15 14 adantl ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝑇 ∈ ℕ0* → ( 𝑇 ≤ 𝑆 → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
16 15 imp32 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
17 16 ralimdv ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
18 17 ex ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
19 18 com23 ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
20 19 a1d ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
21 20 3imp1 ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
22 simpl1l ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → 𝐺 ∈ V )
23 simprl ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → 𝑇 ∈ ℕ0* )
24 1 isewlk ⊢ ( ( 𝐺 ∈ V ∧ 𝑇 ∈ ℕ0* ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
25 22 23 3 24 syl3anc ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑇 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
26 3 21 25 mpbir2and ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ∧ ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) ) → 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) )
27 26 ex ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) ) )
28 2 27 syl ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) ) )
29 28 3impib ⊢ ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆 ) → 𝐹 ∈ ( 𝐺 EdgWalks 𝑇 ) )