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 29739

Description: Lemma 1 for pthd 29742. (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 14420	. . . . . . . 8 ⊢ (𝑃 ∈ Word V → 𝑃:(0..^(♯‘𝑃))⟶V)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑃:(0..^(♯‘𝑃))⟶V)
4		fzo0ss1 13584	. . . . . . . . 9 ⊢ (1..^𝑅) ⊆ (0..^𝑅)
5		pthd.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((♯‘𝑃) − 1)
6	5	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 = ((♯‘𝑃) − 1))
7	6	oveq2d 7357	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑅) = (0..^((♯‘𝑃) − 1)))
8	4, 7	sseqtrid 3972	. . . . . . . 8 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^((♯‘𝑃) − 1)))
9		lencl 14435	. . . . . . . . 9 ⊢ (𝑃 ∈ Word V → (♯‘𝑃) ∈ ℕ₀)
10		nn0z 12488	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
11		fzossrbm1 13583	. . . . . . . . 9 ⊢ ((♯‘𝑃) ∈ ℤ → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
12	1, 9, 10, 11	4syl 19	. . . . . . . 8 ⊢ (𝜑 → (0..^((♯‘𝑃) − 1)) ⊆ (0..^(♯‘𝑃)))
13	8, 12	sstrd 3940	. . . . . . 7 ⊢ (𝜑 → (1..^𝑅) ⊆ (0..^(♯‘𝑃)))
14	3, 13	fssresd 6685	. . . . . 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 12385	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
20	19	ltm1d 12049	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) < (♯‘𝑃))
21		1re 11107	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
22		peano2rem 11423	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑃) ∈ ℝ → ((♯‘𝑃) − 1) ∈ ℝ)
23	19, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℝ)
24		lttr 11184	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ((♯‘𝑃) − 1) ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
25	21, 23, 19, 24	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((1 < ((♯‘𝑃) − 1) ∧ ((♯‘𝑃) − 1) < (♯‘𝑃)) → 1 < (♯‘𝑃)))
26		1red 11108	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑃) ∈ ℕ₀ → 1 ∈ ℝ)
27		ltle 11196	. . . . . . . . . . . . . . . . 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 12421	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℕ ↔ ((♯‘𝑃) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝑃)))
33	31, 32	sylibr 234	. . . . . . . . . . . 12 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
34	18, 33	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℕ)
35		fzo0sn0fzo1 13650	. . . . . . . . . . 11 ⊢ ((♯‘𝑃) ∈ ℕ → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ (1..^(♯‘𝑃))))
37		1zzd 12498	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → 1 ∈ ℤ)
38		1p1e2 12240	. . . . . . . . . . . . . . . 16 ⊢ (1 + 1) = 2
39		2z 12499	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
40	38, 39	eqeltri 2827	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) ∈ ℤ
41	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (1 + 1) ∈ ℤ)
42	10	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ ℤ)
43		ltaddsub 11586	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → ((1 + 1) < (♯‘𝑃) ↔ 1 < ((♯‘𝑃) − 1)))
44	43	bicomd 223	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑃) ∈ ℝ) → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
45	21, 26, 19, 44	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (1 < ((♯‘𝑃) − 1) ↔ (1 + 1) < (♯‘𝑃)))
46		2re 12194	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
47	38, 46	eqeltri 2827	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 1) ∈ ℝ
48		ltle 11196	. . . . . . . . . . . . . . . . 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 12733	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)) ↔ ((1 + 1) ∈ ℤ ∧ (♯‘𝑃) ∈ ℤ ∧ (1 + 1) ≤ (♯‘𝑃)))
53	41, 42, 51, 52	syl3anbrc 1344	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
54	18, 53	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1)))
55		fzosplitsnm1 13635	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ (♯‘𝑃) ∈ (ℤ_≥‘(1 + 1))) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
56	37, 54, 55	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (1..^(♯‘𝑃)) = ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))
57	56	uneq2d 4113	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → ({0} ∪ (1..^(♯‘𝑃))) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
58	36, 57	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (0..^(♯‘𝑃)) = ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})))
59	58	raleqdv 3292	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
60		ralunb 4142	. . . . . . . . 9 ⊢ (∀𝑖 ∈ ({0} ∪ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)}))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (∀𝑖 ∈ {0}∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ∧ ∀𝑖 ∈ ((1..^((♯‘𝑃) − 1)) ∪ {((♯‘𝑃) − 1)})∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))))
61		ralunb 4142	. . . . . . . . . 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 2740	. . . . . . . . . . . 12 ⊢ ((♯‘𝑃) − 1) = 𝑅
66	65	oveq2i 7352	. . . . . . . . . . 11 ⊢ (1..^((♯‘𝑃) − 1)) = (1..^𝑅)
67	66	raleqi 3290	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1..^((♯‘𝑃) − 1))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑖 ∈ (1..^𝑅)∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))
68		fvres 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑖) = (𝑃‘𝑖))
69	68	eqcomd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1..^𝑅) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
70	69	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
71	70	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑖) = ((𝑃 ↾ (1..^𝑅))‘𝑖))
72		fvres 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1..^𝑅) → ((𝑃 ↾ (1..^𝑅))‘𝑗) = (𝑃‘𝑗))
73	72	eqcomd 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝑅) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
74	73	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (𝑃‘𝑗) = ((𝑃 ↾ (1..^𝑅))‘𝑗))
75	71, 74	neeq12d 2989	. . . . . . . . . . . . . 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 3144	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 1 < ((♯‘𝑃) − 1)) ∧ 𝑖 ∈ (1..^𝑅)) → (∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → ((𝑃 ↾ (1..^𝑅))‘𝑖) ≠ ((𝑃 ↾ (1..^𝑅))‘𝑗))))
79	78	ralimdva 3144	. . . . . . . . . 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 7199	. . . . 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 6481	. . . 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 6542	. . 3 ⊢ Fun ^◡∅
91	18	nn0zd 12489	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝑃) ∈ ℤ)
92		peano2zm 12510	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
93	91, 92	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℤ)
94	93	zred 12572	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝑃) − 1) ∈ ℝ)
95		1red 11108	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
96	94, 95	lenltd 11254	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝑃) − 1) ≤ 1 ↔ ¬ 1 < ((♯‘𝑃) − 1)))
97	96	biimpar 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ((♯‘𝑃) − 1) ≤ 1)
98	5, 97	eqbrtrid 5121	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → 𝑅 ≤ 1)
99		1zzd 12498	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℤ)
100	5, 93	eqeltrid 2835	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℤ)
101	99, 100	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
102	101	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (1 ∈ ℤ ∧ 𝑅 ∈ ℤ))
103		fzon 13575	. . . . . . . . . 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 5923	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = (𝑃 ↾ ∅))
108		res0 5927	. . . . . 6 ⊢ (𝑃 ↾ ∅) = ∅
109	107, 108	eqtrdi 2782	. . . . 5 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (𝑃 ↾ (1..^𝑅)) = ∅)
110	109	cnveqd 5810	. . . 4 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → ^◡(𝑃 ↾ (1..^𝑅)) = ^◡∅)
111	110	funeqd 6498	. . 3 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → (Fun ^◡(𝑃 ↾ (1..^𝑅)) ↔ Fun ^◡∅))
112	90, 111	mpbiri 258	. 2 ⊢ ((𝜑 ∧ ¬ 1 < ((♯‘𝑃) − 1)) → Fun ^◡(𝑃 ↾ (1..^𝑅)))
113	89, 112	pm2.61dan 812	1 ⊢ (𝜑 → Fun ^◡(𝑃 ↾ (1..^𝑅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ∪ cun 3895 ⊆ wss 3897 ∅c0 4278 {csn 4571 class class class wbr 5086 ^◡ccnv 5610 ↾ cres 5613 Fun wfun 6470 ⟶wf 6472 –1-1→wf1 6473 ‘cfv 6476 (class class class)co 7341 ℝcr 11000 0cc0 11001 1c1 11002 + caddc 11004 < clt 11141 ≤ cle 11142 − cmin 11339 ℕcn 12120 2c2 12175 ℕ₀cn0 12376 ℤcz 12463 ℤ_≥cuz 12727 ..^cfzo 13549 ♯chash 14232 Word cword 14415

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-card 9827 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-2 12183 df-n0 12377 df-z 12464 df-uz 12728 df-fz 13403 df-fzo 13550 df-hash 14233 df-word 14416

This theorem is referenced by: pthd 29742

W3C validator