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 𝑇 ) )