wlklnwwlkln2lem

		Ref	Expression
	Hypothesis	wlklnwwlkln2lem.1	$⊢ φ \to (P \in WWalks (G) \to \exists f f Walks (G) P)$
	Assertion	wlklnwwlkln2lem	$⊢ φ \to (P \in (N WWalksN G) \to \exists f (f Walks (G) P \land \|f\| = N))$

Proof

Step	Hyp	Ref	Expression
1		wlklnwwlkln2lem.1	$⊢ φ \to (P \in WWalks (G) \to \exists f f Walks (G) P)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wwlknbp	$⊢ P \in (N WWalksN G) \to (G \in V \land N \in ℕ_{0} \land P \in Word Vtx (G))$
4		iswwlksn	$⊢ N \in ℕ_{0} \to (P \in (N WWalksN G) \leftrightarrow (P \in WWalks (G) \land \|P\| = N + 1))$
5	4	adantr	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to (P \in (N WWalksN G) \leftrightarrow (P \in WWalks (G) \land \|P\| = N + 1))$
6		lencl	$⊢ P \in Word Vtx (G) \to \|P\| \in ℕ_{0}$
7	6	nn0cnd	$⊢ P \in Word Vtx (G) \to \|P\| \in ℂ$
8	7	adantl	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to \|P\| \in ℂ$
9		1cnd	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to 1 \in ℂ$
10		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
11	10	adantr	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to N \in ℂ$
12	8 9 11	subadd2d	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to (\|P\| - 1 = N \leftrightarrow N + 1 = \|P\|)$
13		eqcom	$⊢ N + 1 = \|P\| \leftrightarrow \|P\| = N + 1$
14	12 13	bitr2di	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to (\|P\| = N + 1 \leftrightarrow \|P\| - 1 = N)$
15	14	biimpcd	$⊢ \|P\| = N + 1 \to ((N \in ℕ_{0} \land P \in Word Vtx (G)) \to \|P\| - 1 = N)$
16	15	adantl	$⊢ (P \in WWalks (G) \land \|P\| = N + 1) \to ((N \in ℕ_{0} \land P \in Word Vtx (G)) \to \|P\| - 1 = N)$
17	16	impcom	$⊢ ((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \to \|P\| - 1 = N$
18	1	com12	$⊢ P \in WWalks (G) \to (φ \to \exists f f Walks (G) P)$
19	18	adantr	$⊢ (P \in WWalks (G) \land \|P\| = N + 1) \to (φ \to \exists f f Walks (G) P)$
20	19	adantl	$⊢ ((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \to (φ \to \exists f f Walks (G) P)$
21	20	imp	$⊢ (((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \to \exists f f Walks (G) P$
22		simpr	$⊢ ((((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \land f Walks (G) P) \to f Walks (G) P$
23		wlklenvm1	$⊢ f Walks (G) P \to \|f\| = \|P\| - 1$
24	22 23	jccir	$⊢ ((((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \land f Walks (G) P) \to (f Walks (G) P \land \|f\| = \|P\| - 1)$
25	24	ex	$⊢ (((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \to (f Walks (G) P \to (f Walks (G) P \land \|f\| = \|P\| - 1))$
26	25	eximdv	$⊢ (((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \to (\exists f f Walks (G) P \to \exists f (f Walks (G) P \land \|f\| = \|P\| - 1))$
27	21 26	mpd	$⊢ (((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \to \exists f (f Walks (G) P \land \|f\| = \|P\| - 1)$
28		eqeq2	$⊢ \|P\| - 1 = N \to (\|f\| = \|P\| - 1 \leftrightarrow \|f\| = N)$
29	28	anbi2d	$⊢ \|P\| - 1 = N \to ((f Walks (G) P \land \|f\| = \|P\| - 1) \leftrightarrow (f Walks (G) P \land \|f\| = N))$
30	29	exbidv	$⊢ \|P\| - 1 = N \to (\exists f (f Walks (G) P \land \|f\| = \|P\| - 1) \leftrightarrow \exists f (f Walks (G) P \land \|f\| = N))$
31	27 30	imbitrid	$⊢ \|P\| - 1 = N \to ((((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \land φ) \to \exists f (f Walks (G) P \land \|f\| = N))$
32	31	expd	$⊢ \|P\| - 1 = N \to (((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N)))$
33	17 32	mpcom	$⊢ ((N \in ℕ_{0} \land P \in Word Vtx (G)) \land (P \in WWalks (G) \land \|P\| = N + 1)) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N))$
34	33	ex	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to ((P \in WWalks (G) \land \|P\| = N + 1) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N)))$
35	5 34	sylbid	$⊢ (N \in ℕ_{0} \land P \in Word Vtx (G)) \to (P \in (N WWalksN G) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N)))$
36	35	3adant1	$⊢ (G \in V \land N \in ℕ_{0} \land P \in Word Vtx (G)) \to (P \in (N WWalksN G) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N)))$
37	3 36	mpcom	$⊢ P \in (N WWalksN G) \to (φ \to \exists f (f Walks (G) P \land \|f\| = N))$
38	37	com12	$⊢ φ \to (P \in (N WWalksN G) \to \exists f (f Walks (G) P \land \|f\| = N))$

Metamath Proof Explorer

Theorem wlklnwwlkln2lem

Proof