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 30052

Description: Lemma 1 for pthd 30055. (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 14551	. . . . . . . 8 ⊢ (𝑃 ∈ Word V → 𝑃:(0..^(♯‘𝑃))⟶V)
3	1, 2	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃:(0..^(♯‘𝑃))⟶V)
4		fzo0ss1 13714	. . . . . . . . 9 ⊢ (1..^𝑅) ⊆ (0..^𝑅)
5		pthd.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((♯‘𝑃) − 1)
6	5	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 = ((♯‘𝑃) − 1))
7	6	oveq2d 7424	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑅) = (0..^((♯‘𝑃) − 1)))
8	4, 7	sseqtrid 3987	. . . . . . . 8 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^((♯‘𝑃) − 1)))
9		lencl 14566	. . . . . . . . 9 ⊢ (𝑃 ∈ Word V → (♯‘𝑃) ∈ ℕ₀)
10		nn0z 12611	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
11		fzossrbm1 13713	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℤ → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
12	1, 9, 10, 11	4syl 20	. . . . . . . 8 ⊢ (𝜑 → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
13	8, 12	sstrd 3955	. . . . . . 7 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^(♯‘𝑃)))
14	3, 13	fssresd 6743	. . . . . 6 ⊢ (𝜑 → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V)
15	14	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V)
16		pthd.s	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
17	16	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
18	1, 9	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑃) ∈ ℕ₀)
19		nn0re 12509	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
20	19	ltm1d 12143	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) < (♯‘𝑃))
21		1re 11204	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
22		peano2rem 11521	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑃) ∈ ℝ → ((♯‘𝑃) − 1) ∈ ℝ)
23	19, 22	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℝ)
24		lttr 11282	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ((♯‘𝑃) − 1) ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
25	21, 23, 19, 24	mp3an2i 1492	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
26		1red 11205	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 1 ∈ ℝ)
27		ltle 11294	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → (1 < (♯‘𝑃) → 1 ≤ (♯‘𝑃)))
28	26, 19, 27	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < (♯‘𝑃) → 1 ≤ (♯‘𝑃)))
29	25, 28	syld 48	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 ≤ (♯‘𝑃)))
30	20, 29	mpan2d 706	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) → 1 ≤ (♯‘𝑃)))
31	30	imdistani 578	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝑃)))
32		elnnnn0c 12545	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℕ ↔ ((♯‘𝑃) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝑃)))
33	31, 32	sylibr 237	. . . . . . . . . . . 12 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
34	18, 33	sylan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
35		fzo0sn0fzo1 13780	. . . . . . . . . . 11 ⊢ ((♯‘𝑃) ∈ ℕ → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
36	34, 35	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
37		1zzd 12621	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → 1 ∈ ℤ)
38		1p1e2 12360	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
39		2z 12622	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
40	38, 39	eqeltri 2865	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) ∈ ℤ
41	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (1 + 1) ∈ ℤ)
42	10	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℤ)
43		ltaddsub 11684	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 + 1) < (♯‘𝑃) ↔ 1 < ((♯‘𝑃) − 1)))
44	43	bicomd 226	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
45	21, 26, 19, 44	mp3an2i 1492	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
46		2re 12311	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
47	38, 46	eqeltri 2865	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) ∈ ℝ
48		ltle 11294	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + 1) ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 + 1) < (♯‘𝑃) → (1 + 1) ≤ (♯‘𝑃)))
49	47, 19, 48	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 + 1) < (♯‘𝑃) → (1 + 1) ≤ (♯‘𝑃)))
50	45, 49	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) → (1 + 1) ≤ (♯‘𝑃)))
51	50	imp 411	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (1 + 1) ≤ (♯‘𝑃))
52		eluz2 12864	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)) ↔ ((1 + 1) ∈ ℤ ∧ (♯‘𝑃) ∈ ℤ ∧ (1 + 1) ≤ (♯‘𝑃)))
53	41, 42, 51, 52	syl3anbrc 1360	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
54	18, 53	sylan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
55		fzosplitsnm1 13765	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1))) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
56	37, 54, 55	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
57	56	uneq2d 4130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ({0} ∪ (1..^(♯‘𝑃))) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
58	36, 57	eqtrd 2804	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
59	58	raleqdv 3329	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
60		ralunb 4158	. . . . . . . . 9 ⊢ (∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
61		ralunb 4158	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
62	61	anbi2i 634	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))))
63	60, 62	bitri 278	. . . . . . . 8 ⊢ (∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))))
64	59, 63	bitrdi 290	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))))
65	5	eqcomi 2778	. . . . . . . . . . . 12 ⊢ ((♯‘𝑃) − 1) = 𝑅
66	65	oveq2i 7419	. . . . . . . . . . 11 ⊢ (1..^((♯‘𝑃) − 1)) = (1..^𝑅)
67	66	raleqi 3327	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
68		fvres 6898	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑖) = (𝑃‘𝑖))
69	68	eqcomd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1..^𝑅) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
70	69	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
71	70	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
72		fvres 6898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑗) = (𝑃‘𝑗))
73	72	eqcomd 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝑅) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
74	73	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
75	71, 74	neeq12d 3025	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) ↔ ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
76	75	biimpd 232	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
77	76	imim2d 58	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → ((𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
78	77	ralimdva 3183	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
79	78	ralimdva 3183	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
80	67, 79	biimtrid 245	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
81	80	adantrd 496	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
82	81	adantld 495	. . . . . . 7 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ {((♯‘𝑃) − 1)}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
83	64, 82	sylbid 243	. . . . . 6 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
84	17, 83	mpd 16	. . . . 5 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗)))
85		dff14a 7266	. . . . 5 ⊢ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V ↔ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
86	15, 84, 85	sylanbrc 594	. . . 4 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V)
87		df-f1 6538	. . . 4 ⊢ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)–1-1→V ↔ ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ Fun ^◡(𝑃 ↾ (1..^𝑅))))
88	86, 87	sylib 221	. . 3 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ((𝑃 ↾ (1..^𝑅)):(1..^𝑅)⟶V ∧ Fun ^◡(𝑃 ↾ (1..^𝑅))))
89	88	simprd 500	. 2 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → Fun ^◡(𝑃 ↾ (1..^𝑅)))
90		funcnv0 6599	. . 3 ⊢ Fun ^◡∅
91	18	nn0zd 12612	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝑃) ∈ ℤ)
92		peano2zm 12633	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
93	91, 92	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℤ)
94	93	zred 12696	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℝ)
95		1red 11205	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
96	94, 95	lenltd 11352	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝑃) − 1) ≤ 1 ↔ ¬ 1 < ((♯‘𝑃) − 1)))
97	96	biimpar 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) − 1) ≤ 1)
98	5, 97	eqbrtrid 5147	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → 𝑅 ≤ 1)
99		1zzd 12621	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℤ)
100	5, 93	eqeltrid 2873	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℤ)
101	99, 100	jca 520	. . . . . . . . . 10 ⊢ (𝜑 → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
102	101	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
103		fzon 13705	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑅 ≤ 1 ↔ (1..^𝑅) = ∅))
104	103	bicomd 226	. . . . . . . . 9 ⊢ ((1 ∈ ℤ ∧ 𝑅 ∈ ℤ) → ((1..^𝑅) = ∅ ↔ 𝑅 ≤ 1))
105	102, 104	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ((1..^𝑅) = ∅ ↔ 𝑅 ≤ 1))
106	98, 105	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (1..^𝑅) = ∅)
107	106	reseq2d 5976	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = (𝑃 ↾ ∅))
108		res0 5980	. . . . . 6 ⊢ (𝑃 ↾ ∅) = ∅
109	107, 108	eqtrdi 2820	. . . . 5 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = ∅)
110	109	cnveqd 5859	. . . 4 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ^◡(𝑃 ↾ (1..^𝑅)) = ^◡∅)
111	110	funeqd 6555	. . 3 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (Fun ^◡(𝑃 ↾ (1..^𝑅)) ↔ Fun ^◡∅))
112	90, 111	mpbiri 261	. 2 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → Fun ^◡(𝑃 ↾ (1..^𝑅)))
113	89, 112	pm2.61dan 824	1 ⊢ (𝜑 → Fun ^◡(𝑃 ↾ (1..^𝑅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 Vcvv 3463 ∪ cun 3911 ⊆ wss 3913 ∅c0 4294 {csn 4591 class class class wbr 5110 ^◡ccnv 5658 ↾ cres 5661 Fun wfun 6527 ⟶wf 6529 –1-1→wf1 6530 ‘cfv 6533 (class class class)co 7408 ℝcr 11095 0cc0 11096 1c1 11097 + caddc 11099 < clt 11239 ≤ cle 11240 − cmin 11437 ℕcn 12229 2c2 12291 ℕ₀cn0 12500 ℤcz 12587 ℤ_≥cuz 12858 ..^cfzo 13678 ♯chash 14362 Word cword 14546

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9921 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-nn 12230 df-2 12299 df-n0 12501 df-z 12588 df-uz 12859 df-fz 13532 df-fzo 13679 df-hash 14363 df-word 14547

This theorem is referenced by: pthd 30055

W3C validator