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	$⊢ (F \in (G EdgWalks S) \land T \in ℕ_{0}^{*} \land T \leq S) \to F \in (G EdgWalks T)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	ewlkprop	$⊢ F \in (G EdgWalks S) \to ((G \in V \land S \in ℕ_{0}^{*}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
3		simpl2	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to F \in Word dom iEdg (G)$
4		xnn0xr	$⊢ T \in ℕ_{0}^{} \to T \in ℝ^{}$
5	4	adantl	$⊢ (S \in ℕ_{0}^{} \land T \in ℕ_{0}^{}) \to T \in ℝ^{*}$
6		xnn0xr	$⊢ S \in ℕ_{0}^{} \to S \in ℝ^{}$
7	6	adantr	$⊢ (S \in ℕ_{0}^{} \land T \in ℕ_{0}^{}) \to S \in ℝ^{*}$
8		fvex	$⊢ iEdg (G) (F (k - 1)) \in V$
9	8	inex1	$⊢ iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k)) \in V$
10		hashxrcl	$⊢ iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k)) \in V \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{*}$
11	9 10	mp1i	$⊢ (S \in ℕ_{0}^{} \land T \in ℕ_{0}^{}) \to \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{*}$
12		xrletr	$⊢ (T \in ℝ^{} \land S \in ℝ^{} \land \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \in ℝ^{*}) \to ((T \leq S \land S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
13	5 7 11 12	syl3anc	$⊢ (S \in ℕ_{0}^{} \land T \in ℕ_{0}^{}) \to ((T \leq S \land S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
14	13	exp4b	$⊢ S \in ℕ_{0}^{} \to (T \in ℕ_{0}^{} \to (T \leq S \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)))$
15	14	adantl	$⊢ (G \in V \land S \in ℕ_{0}^{}) \to (T \in ℕ_{0}^{} \to (T \leq S \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)))$
16	15	imp32	$⊢ ((G \in V \land S \in ℕ_{0}^{}) \land (T \in ℕ_{0}^{} \land T \leq S)) \to (S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
17	16	ralimdv	$⊢ ((G \in V \land S \in ℕ_{0}^{}) \land (T \in ℕ_{0}^{} \land T \leq S)) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)$
18	17	ex	$⊢ (G \in V \land S \in ℕ_{0}^{}) \to ((T \in ℕ_{0}^{} \land T \leq S) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|))$
19	18	com23	$⊢ (G \in V \land S \in ℕ_{0}^{}) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to ((T \in ℕ_{0}^{} \land T \leq S) \to \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|))$
20	19	a1d	$⊢ (G \in V \land S \in ℕ_{0}^{}) \to (F \in Word dom iEdg (G) \to (\forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\| \to ((T \in ℕ_{0}^{} \land T \leq S) \to \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|)))$
21	20	3imp1	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|$
22		simpl1l	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to G \in V$
23		simprl	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to T \in ℕ_{0}^{*}$
24	1	isewlk	$⊢ (G \in V \land T \in ℕ_{0}^{*} \land F \in Word dom iEdg (G)) \to (F \in (G EdgWalks T) \leftrightarrow (F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|))$
25	22 23 3 24	syl3anc	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to (F \in (G EdgWalks T) \leftrightarrow (F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) T \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|))$
26	3 21 25	mpbir2and	$⊢ (((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \land (T \in ℕ_{0}^{} \land T \leq S)) \to F \in (G EdgWalks T)$
27	26	ex	$⊢ ((G \in V \land S \in ℕ_{0}^{}) \land F \in Word dom iEdg (G) \land \forall k \in (1 ..^\|F\|) S \leq \|iEdg (G) (F (k - 1)) \cap iEdg (G) (F (k))\|) \to ((T \in ℕ_{0}^{} \land T \leq S) \to F \in (G EdgWalks T))$
28	2 27	syl	$⊢ F \in (G EdgWalks S) \to ((T \in ℕ_{0}^{*} \land T \leq S) \to F \in (G EdgWalks T))$
29	28	3impib	$⊢ (F \in (G EdgWalks S) \land T \in ℕ_{0}^{*} \land T \leq S) \to F \in (G EdgWalks T)$

Metamath Proof Explorer

Theorem ewlkle

Proof