Theorem clwlkclwwlklem2fv2

Description: Lemma 4b for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 22-Jun-2018)

	Ref	Expression
Hypothesis	clwlkclwwlklem2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion	clwlkclwwlklem2fv2	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlklem2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2		simpr	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) )
3		nn0z	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
4		2z	⊢ 2 ∈ ℤ
5	3 4	jctir	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) )
6		zsubcl	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
7	5 6	syl	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
8	7	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
9	8	adantr	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
10	2 9	eqeltrd	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 𝑥 ∈ ℤ )
11	10	ex	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → 𝑥 ∈ ℤ ) )
12		zre	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
13		nn0re	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
14		2re	⊢ 2 ∈ ℝ
15	14	a1i	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℝ )
16	13 15	resubcld	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
17	16	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
18		lttri3	⊢ ( ( 𝑥 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) ) )
19	12 17 18	syl2anr	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) ) )
20		simpl	⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
21	19 20	syl6bi	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
22	21	ex	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ℤ → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
23	11 22	syld	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
24	23	com13	⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
25	24	pm2.43i	⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
26	25	impcom	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
27	26	iffalsed	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) )
28		fveq2	⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
29	28	adantl	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
30	29	preq1d	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } )
31	30	fveq2d	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )
32	27 31	eqtrd	⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )
33	5	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) )
34	33 6	syl	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
35	13 15	subge0d	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
36	35	biimpar	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) )
37		elnn0z	⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
38	34 36 37	sylanbrc	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 )
39		nn0ge2m1nn	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ )
40		1red	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 1 ∈ ℝ )
41	14	a1i	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ∈ ℝ )
42	13	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℝ )
43		1lt2	⊢ 1 < 2
44	43	a1i	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 1 < 2 )
45	40 41 42 44	ltsub2dd	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) < ( ( ♯ ‘ 𝑃 ) − 1 ) )
46		elfzo0	⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) < ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
47	38 39 45 46	syl3anbrc	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
48		fvexd	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) ∈ V )
49	1 32 47 48	fvmptd2	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )