pthdlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pthdlem1		Structured version Visualization version GIF version

Theorem pthdlem1 29799

Description: Lemma 1 for pthd 29802. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)

**Hypotheses**
Ref	Expression
pthd.p	⊢ (𝜑 → 𝑃 ∈ Word V)
pthd.r	⊢ 𝑅 = ((♯‘𝑃) − 1)
pthd.s	⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))

**Assertion**
Ref	Expression
pthdlem1	⊢ (𝜑 → Fun ^◡(𝑃 ↾ (1..^𝑅)))

Distinct variable groups: 𝑃,𝑖,𝑗 𝑅,𝑖,𝑗 𝜑,𝑖,𝑗

**Proof of Theorem pthdlem1**
Step	Hyp	Ref	Expression
1		pthd.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ Word V)
2		wrdf 14554	. . . . . . . 8 ⊢ (𝑃 ∈ Word V → 𝑃:(0..^(♯‘𝑃))⟶V)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑃:(0..^(♯‘𝑃))⟶V)
4		fzo0ss1 13726	. . . . . . . . 9 ⊢ (1..^𝑅) ⊆ (0..^𝑅)
5		pthd.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((♯‘𝑃) − 1)
6	5	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 = ((♯‘𝑃) − 1))
7	6	oveq2d 7447	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑅) = (0..^((♯‘𝑃) − 1)))
8	4, 7	sseqtrid 4048	. . . . . . . 8 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^((♯‘𝑃) − 1)))
9		lencl 14568	. . . . . . . . 9 ⊢ (𝑃 ∈ Word V → (♯‘𝑃) ∈ ℕ₀)
10		nn0z 12636	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
11		fzossrbm1 13725	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℤ → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
12	1, 9, 10, 11	4syl 19	. . . . . . . 8 ⊢ (𝜑 → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
13	8, 12	sstrd 4006	. . . . . . 7 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^(♯‘𝑃)))
14	3, 13	fssresd 6776	. . . . . 6 ⊢ (𝜑 → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V)
15	14	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V)
16		pthd.s	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
18	1, 9	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑃) ∈ ℕ₀)
19		nn0re 12533	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
20	19	ltm1d 12198	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) < (♯‘𝑃))
21		1re 11259	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
22		peano2rem 11574	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑃) ∈ ℝ → ((♯‘𝑃) − 1) ∈ ℝ)
23	19, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℝ)
24		lttr 11335	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ((♯‘𝑃) − 1) ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
25	21, 23, 19, 24	mp3an2i 1465	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
26		1red 11260	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 1 ∈ ℝ)
27		ltle 11347	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → (1 < (♯‘𝑃) → 1 ≤ (♯‘𝑃)))
28	26, 19, 27	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < (♯‘𝑃) → 1 ≤ (♯‘𝑃)))
29	25, 28	syld 47	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 ≤ (♯‘𝑃)))
30	20, 29	mpan2d 694	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) → 1 ≤ (♯‘𝑃)))
31	30	imdistani 568	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝑃)))
32		elnnnn0c 12569	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℕ ↔ ((♯‘𝑃) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝑃)))
33	31, 32	sylibr 234	. . . . . . . . . . . 12 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
34	18, 33	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
35		fzo0sn0fzo1 13791	. . . . . . . . . . 11 ⊢ ((♯‘𝑃) ∈ ℕ → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
37		1zzd 12646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → 1 ∈ ℤ)
38		1p1e2 12389	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
39		2z 12647	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
40	38, 39	eqeltri 2835	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) ∈ ℤ
41	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (1 + 1) ∈ ℤ)
42	10	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℤ)
43		ltaddsub 11735	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 + 1) < (♯‘𝑃) ↔ 1 < ((♯‘𝑃) − 1)))
44	43	bicomd 223	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
45	21, 26, 19, 44	mp3an2i 1465	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
46		2re 12338	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
47	38, 46	eqeltri 2835	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) ∈ ℝ
48		ltle 11347	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + 1) ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 + 1) < (♯‘𝑃) → (1 + 1) ≤ (♯‘𝑃)))
49	47, 19, 48	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 + 1) < (♯‘𝑃) → (1 + 1) ≤ (♯‘𝑃)))
50	45, 49	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) → (1 + 1) ≤ (♯‘𝑃)))
51	50	imp 406	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (1 + 1) ≤ (♯‘𝑃))
52		eluz2 12882	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)) ↔ ((1 + 1) ∈ ℤ ∧ (♯‘𝑃) ∈ ℤ ∧ (1 + 1) ≤ (♯‘𝑃)))
53	41, 42, 51, 52	syl3anbrc 1342	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
54	18, 53	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
55		fzosplitsnm1 13776	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1))) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
56	37, 54, 55	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
57	56	uneq2d 4178	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ({0} ∪ (1..^(♯‘𝑃))) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
58	36, 57	eqtrd 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
59	58	raleqdv 3324	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
60		ralunb 4207	. . . . . . . . 9 ⊢ (∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
61		ralunb 4207	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
62	61	anbi2i 623	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))))
63	60, 62	bitri 275	. . . . . . . 8 ⊢ (∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))))
64	59, 63	bitrdi 287	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))))
65	5	eqcomi 2744	. . . . . . . . . . . 12 ⊢ ((♯‘𝑃) − 1) = 𝑅
66	65	oveq2i 7442	. . . . . . . . . . 11 ⊢ (1..^((♯‘𝑃) − 1)) = (1..^𝑅)
67	66	raleqi 3322	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
68		fvres 6926	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑖) = (𝑃‘𝑖))
69	68	eqcomd 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1..^𝑅) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
70	69	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
71	70	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
72		fvres 6926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑗) = (𝑃‘𝑗))
73	72	eqcomd 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝑅) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
74	73	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
75	71, 74	neeq12d 3000	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) ↔ ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
76	75	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
77	76	imim2d 57	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
78	77	ralimdva 3165	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
79	78	ralimdva 3165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
80	67, 79	biimtrid 242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
81	80	adantrd 491	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
82	81	adantld 490	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
83	64, 82	sylbid 240	. . . . . 6 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
84	17, 83	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
85		dff14a 7290	. . . . 5 ⊢ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V ↔ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
86	15, 84, 85	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V)
87		df-f1 6568	. . . 4 ⊢ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V ↔ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ Fun ^◡(𝑃 ↾ (1..^𝑅))))
88	86, 87	sylib 218	. . 3 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ Fun ^◡(𝑃 ↾ (1..^𝑅))))
89	88	simprd 495	. 2 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → Fun ^◡(𝑃 ↾ (1..^𝑅)))
90		funcnv0 6634	. . 3 ⊢ Fun ^◡∅
91	18	nn0zd 12637	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝑃) ∈ ℤ)
92		peano2zm 12658	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
93	91, 92	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℤ)
94	93	zred 12720	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℝ)
95		1red 11260	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
96	94, 95	lenltd 11405	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝑃) − 1) ≤ 1 ↔ ¬ 1 < ((♯‘𝑃) − 1)))
97	96	biimpar 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) − 1) ≤ 1)
98	5, 97	eqbrtrid 5183	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → 𝑅 ≤ 1)
99		1zzd 12646	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℤ)
100	5, 93	eqeltrid 2843	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℤ)
101	99, 100	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
102	101	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
103		fzon 13717	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑅 ≤ 1 ↔ (1..^𝑅) = ∅))
104	103	bicomd 223	. . . . . . . . 9 ⊢ ((1 ∈ ℤ ∧ 𝑅 ∈ ℤ) → ((1..^𝑅) = ∅ ↔ 𝑅 ≤ 1))
105	102, 104	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ((1..^𝑅) = ∅ ↔ 𝑅 ≤ 1))
106	98, 105	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (1..^𝑅) = ∅)
107	106	reseq2d 6000	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = (𝑃 ↾ ∅))
108		res0 6004	. . . . . 6 ⊢ (𝑃 ↾ ∅) = ∅
109	107, 108	eqtrdi 2791	. . . . 5 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = ∅)
110	109	cnveqd 5889	. . . 4 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ^◡(𝑃 ↾ (1..^𝑅)) = ^◡∅)
111	110	funeqd 6590	. . 3 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (Fun ^◡(𝑃 ↾ (1..^𝑅)) ↔ Fun ^◡∅))
112	90, 111	mpbiri 258	. 2 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → Fun ^◡(𝑃 ↾ (1..^𝑅)))
113	89, 112	pm2.61dan 813	1 ⊢ (𝜑 → Fun ^◡(𝑃 ↾ (1..^𝑅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 Vcvv 3478 ∪ cun 3961 ⊆ wss 3963 ∅c0 4339 {csn 4631 class class class wbr 5148 ^◡ccnv 5688 ↾ cres 5691 Fun wfun 6557 ⟶wf 6559 –1-1→wf1 6560 ‘cfv 6563 (class class class)co 7431 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 < clt 11293 ≤ cle 11294 − cmin 11490 ℕcn 12264 2c2 12319 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 ..^cfzo 13691 ♯chash 14366 Word cword 14549

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-nn 12265 df-2 12327 df-n0 12525 df-z 12612 df-uz 12877 df-fz 13545 df-fzo 13692 df-hash 14367 df-word 14550

This theorem is referenced by: pthd 29802

W3C validator