Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑁 ∈
ℕ) |
3 | | poimirlem22.s |
. . . 4
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{m} (1...𝑁))) |
5 | 4 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{m} (1...𝑁))) |
6 | | poimirlem22.2 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
7 | 6 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ 𝑆) |
8 | | simpr 487 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
9 | 2, 3, 5, 7, 8 | poimirlem15 34899 |
. . 3
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
⟨⟨(1^{st} ‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩ ∈ 𝑆) |
10 | | fveq2 6663 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑇)) |
11 | 10 | breq2d 5069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑇))) |
12 | 11 | ifbid 4487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1))) |
13 | 12 | csbeq1d 3885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
14 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑇))) |
15 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
16 | 15 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑗))) |
17 | 16 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1})) |
18 | 15 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
19 | 18 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
20 | 17, 19 | uneq12d 4138 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
21 | 14, 20 | oveq12d 7166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → ((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
22 | 21 | csbeq2dv 3888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
23 | 13, 22 | eqtrd 2854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
24 | 23 | mpteq2dv 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
25 | 24 | eqeq2d 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
26 | 25, 3 | elrab2 3681 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
27 | 26 | simprbi 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
28 | 6, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
29 | 28 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
30 | | elrabi 3673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
31 | 30, 3 | eleq2s 2929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
33 | | xp1st 7713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1^{st}
‘𝑇) ∈
(((0..^𝐾)
↑_{m} (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
35 | | xp1st 7713 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁))) |
37 | | elmapi 8420 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
39 | | elfzoelz 13030 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
40 | 39 | ssriv 3969 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
41 | | fss 6520 |
. . . . . . . . . . . . . . . 16
⊢
(((1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
42 | 38, 40, 41 | sylancl 588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
43 | 42 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
44 | | xp2nd 7714 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
45 | 34, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
46 | | fvex 6676 |
. . . . . . . . . . . . . . . . 17
⊢
(2^{nd} ‘(1^{st} ‘𝑇)) ∈ V |
47 | | f1oeq1 6597 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
48 | 46, 47 | elab 3665 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
49 | 45, 48 | sylib 220 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
50 | 49 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
51 | 2, 29, 43, 50, 8 | poimirlem1 34885 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
52 | 51 | adantr 483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
53 | 1 | ad3antrrr 728 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) → 𝑁 ∈
ℕ) |
54 | | fveq2 6663 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑧)) |
55 | 54 | breq2d 5069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑧))) |
56 | 55 | ifbid 4487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1))) |
57 | 56 | csbeq1d 3885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
58 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑧))) |
59 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑧 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑧))) |
60 | 59 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑗))) |
61 | 60 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1})) |
62 | 59 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
63 | 62 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
64 | 61, 63 | uneq12d 4138 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
65 | 58, 64 | oveq12d 7166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
66 | 65 | csbeq2dv 3888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
67 | 57, 66 | eqtrd 2854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
68 | 67 | mpteq2dv 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
69 | 68 | eqeq2d 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
70 | 69, 3 | elrab2 3681 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
71 | 70 | simprbi 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
72 | 71 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
73 | | elrabi 3673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
74 | 73, 3 | eleq2s 2929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
75 | | xp1st 7713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
77 | | xp1st 7713 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^{st}
‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁))) |
79 | | elmapi 8420 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{m} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
81 | | fss 6520 |
. . . . . . . . . . . . . . . . 17
⊢
(((1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
82 | 80, 40, 81 | sylancl 588 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
83 | 82 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
84 | | xp2nd 7714 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
85 | 76, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
86 | | fvex 6676 |
. . . . . . . . . . . . . . . . . 18
⊢
(2^{nd} ‘(1^{st} ‘𝑧)) ∈ V |
87 | | f1oeq1 6597 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
88 | 86, 87 | elab 3665 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
89 | 85, 88 | sylib 220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
90 | 89 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
91 | | simpllr 774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
92 | | xp2nd 7714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
93 | 74, 92 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
94 | 93 | adantl 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
95 | | eldifsn 4711 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑧) ∈ ((0...𝑁) ∖ {(2^{nd} ‘𝑇)}) ↔ ((2^{nd}
‘𝑧) ∈ (0...𝑁) ∧ (2^{nd}
‘𝑧) ≠
(2^{nd} ‘𝑇))) |
96 | 95 | biimpri 230 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘𝑧) ∈ (0...𝑁) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
97 | 94, 96 | sylan 582 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
98 | 53, 72, 83, 90, 91, 97 | poimirlem2 34886 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
99 | 98 | ex 415 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛))) |
100 | 99 | necon1bd 3032 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇))) |
101 | 52, 100 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
102 | | eleq1 2898 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑧) = (2^{nd} ‘𝑇) → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
103 | 102 | biimparc 482 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1))) |
104 | 103 | anim2i 618 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
105 | 104 | anassrs 470 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
106 | 71 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
107 | | breq1 5060 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → (𝑦 < (2^{nd} ‘𝑧) ↔ 0 < (2^{nd}
‘𝑧))) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → 𝑦 = 0) |
109 | 107, 108 | ifbieq1d 4488 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0 → if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1))) |
110 | | elfznn 12928 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑧) ∈
ℕ) |
111 | 110 | nngt0d 11678 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^{nd}
‘𝑧)) |
112 | 111 | iftrued 4473 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 <
(2^{nd} ‘𝑧),
0, (𝑦 + 1)) =
0) |
113 | 112 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1)) = 0) |
114 | 109, 113 | sylan9eqr 2876 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1)) = 0) |
115 | 114 | csbeq1d 3885 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
116 | | c0ex 10627 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
117 | | oveq2 7156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
118 | | fz10 12920 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1...0) =
∅ |
119 | 117, 118 | syl6eq 2870 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
120 | 119 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
∅)) |
121 | 120 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ∅) ×
{1})) |
122 | | oveq1 7155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
123 | | 0p1e1 11751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
124 | 122, 123 | syl6eq 2870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
125 | 124 | oveq1d 7163 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
126 | 125 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑁))) |
127 | 126 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
128 | 121, 127 | uneq12d 4138 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 0 → ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}))) |
129 | | ima0 5938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) =
∅ |
130 | 129 | xpeq1i 5574 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) = (∅
× {1}) |
131 | | 0xp 5642 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
× {1}) = ∅ |
132 | 130, 131 | eqtri 2842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) =
∅ |
133 | 132 | uneq1i 4133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
134 | | uncom 4127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∪ (((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪
∅) |
135 | | un0 4342 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
136 | 133, 134,
135 | 3eqtri 2846 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
137 | 128, 136 | syl6eq 2870 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
138 | 137 | oveq2d 7164 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 0 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}))) |
139 | 116, 138 | csbie 3916 |
. . . . . . . . . . . . . . . . 17
⊢
⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
140 | | f1ofo 6615 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
141 | 89, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
142 | | foima 6588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
144 | 143 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
145 | 144 | oveq2d 7164 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((1...𝑁) ×
{0}))) |
146 | | ovexd 7183 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V) |
147 | 80 | ffnd 6508 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)) Fn (1...𝑁)) |
148 | | fnconstg 6560 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
149 | 116, 148 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
150 | | eqidd 2820 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) = ((1^{st} ‘(1^{st}
‘𝑧))‘𝑛)) |
151 | 116 | fvconst2 6959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
152 | 151 | adantl 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
153 | 80 | ffvelrnda 6844 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾)) |
154 | | elfzonn0 13074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1^{st} ‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
156 | 155 | nn0cnd 11949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ ℂ) |
157 | 156 | addid1d 10832 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) + 0) = ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛)) |
158 | 146, 147,
149, 147, 150, 152, 157 | offveq 7422 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((1...𝑁) × {0})) =
(1^{st} ‘(1^{st} ‘𝑧))) |
159 | 145, 158 | eqtrd 2854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (1^{st}
‘(1^{st} ‘𝑧))) |
160 | 139, 159 | syl5eq 2866 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
161 | 160 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
162 | 115, 161 | eqtrd 2854 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
163 | | nnm1nn0 11930 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ_{0}) |
164 | 1, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ_{0}) |
165 | | 0elfz 12996 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈
ℕ_{0} → 0 ∈ (0...(𝑁 − 1))) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
167 | 166 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1))) |
168 | | fvexd 6678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) ∈ V) |
169 | 106, 162,
167, 168 | fvmptd 6768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
170 | 105, 169 | sylan 582 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
171 | 170 | an32s 650 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
172 | 101, 171 | mpdan 685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
173 | | fveq2 6663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
174 | 173 | eleq1d 2895 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
175 | 174 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))))) |
176 | | 2fveq3 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
177 | 176 | eqeq2d 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)) ↔ (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
178 | 175, 177 | imbi12d 347 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) ↔ ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))))) |
179 | 169 | expcom 416 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)))) |
180 | 178, 179 | vtoclga 3572 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
181 | 7, 180 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝐹‘0) =
(1^{st} ‘(1^{st} ‘𝑇))) |
182 | 181 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))) |
183 | 172, 182 | eqtr3d 2856 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
184 | 183 | adantr 483 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
185 | 1 | ad3antrrr 728 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ) |
186 | 6 | ad3antrrr 728 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆) |
187 | | simpllr 774 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) |
188 | | simplr 767 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆) |
189 | 34 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘𝑇)
∈ (((0..^𝐾)
↑_{m} (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
190 | | xpopth 7722 |
. . . . . . . . . . . . . 14
⊢
(((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) ↔
(1^{st} ‘𝑧) =
(1^{st} ‘𝑇))) |
191 | 76, 189, 190 | syl2anr 598 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) ↔
(1^{st} ‘𝑧) =
(1^{st} ‘𝑇))) |
192 | 32 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
193 | | xpopth 7722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) ↔ 𝑧 = 𝑇)) |
194 | 193 | biimpd 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) → 𝑧 = 𝑇)) |
195 | 74, 192, 194 | syl2anr 598 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) → 𝑧 = 𝑇)) |
196 | 101, 195 | mpan2d 692 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((1^{st} ‘𝑧) = (1^{st} ‘𝑇) → 𝑧 = 𝑇)) |
197 | 191, 196 | sylbid 242 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) → 𝑧 = 𝑇)) |
198 | 183, 197 | mpand 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇)) → 𝑧 = 𝑇)) |
199 | 198 | necon3d 3035 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇)))) |
200 | 199 | imp 409 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇))) |
201 | 185, 3, 186, 187, 188, 200 | poimirlem9 34893 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd}
‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))) |
202 | 101 | adantr 483 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
203 | 184, 201,
202 | jca31 517 |
. . . . . . 7
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))) |
204 | 203 | ex 415 |
. . . . . 6
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
205 | | simplr 767 |
. . . . . . . 8
⊢
((((1^{st} ‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ (2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))) |
206 | | elfznn 12928 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℕ) |
207 | 206 | nnred 11645 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℝ) |
208 | 207 | ltp1d 11562 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
209 | 207, 208 | ltned 10768 |
. . . . . . . . . . . 12
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
210 | 209 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
≠ ((2^{nd} ‘𝑇) + 1)) |
211 | | fveq1 6662 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})))) →
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇))) |
212 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ∈
ℝ) |
213 | | ltp1 11472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
214 | 212, 213 | ltned 10768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
215 | | fvex 6676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2^{nd} ‘𝑇) ∈ V |
216 | | ovex 7181 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) + 1) ∈ V |
217 | 215, 216,
216, 215 | fpr 6909 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}) |
218 | 214, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}) |
219 | | f1oi 6645 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
220 | | f1of 6608 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) → ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
221 | 219, 220 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
222 | | disjdif 4419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) =
∅ |
223 | | fun 6533 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}
∧ ( I ↾ ((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})) ∧
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ∅) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))):({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) +
1)}))⟶({((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
224 | 222, 223 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}
∧ ( I ↾ ((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))):({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) +
1)}))⟶({((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
225 | 218, 221,
224 | sylancl 588 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))):({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) +
1)}))⟶({((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
226 | 215 | prid1 4690 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} |
227 | | elun1 4150 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} → (2^{nd}
‘𝑇) ∈
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
228 | 226, 227 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2^{nd} ‘𝑇) ∈ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})) |
229 | | fvco3 6753 |
. . . . . . . . . . . . . . . . . . 19
⊢
((({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))):({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) +
1)}))⟶({((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) ∧ (2^{nd}
‘𝑇) ∈
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) →
(((2^{nd} ‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇))‘(({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))‘(2^{nd} ‘𝑇)))) |
230 | 225, 228,
229 | sylancl 588 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇))‘(({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))‘(2^{nd} ‘𝑇)))) |
231 | 218 | ffnd 6508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
232 | | fnresi 6469 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) |
233 | 222, 226 | pm3.2i 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ∅ ∧
(2^{nd} ‘𝑇)
∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
234 | | fvun1 6747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∧ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) ∧ (({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ∅ ∧
(2^{nd} ‘𝑇)
∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) → (({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))‘(2^{nd} ‘𝑇)) = ({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}‘(2^{nd}
‘𝑇))) |
235 | 232, 233,
234 | mp3an23 1446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} →
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})))‘(2^{nd} ‘𝑇)) = ({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}‘(2^{nd}
‘𝑇))) |
236 | 231, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})))‘(2^{nd} ‘𝑇)) = ({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}‘(2^{nd}
‘𝑇))) |
237 | 215, 216 | fvpr1 6945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
238 | 214, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
239 | 236, 238 | eqtrd 2854 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})))‘(2^{nd} ‘𝑇)) = ((2^{nd} ‘𝑇) + 1)) |
240 | 239 | fveq2d 6667 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘𝑇) ∈ ℝ → ((2^{nd}
‘(1^{st} ‘𝑇))‘(({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))‘(2^{nd} ‘𝑇))) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))) |
241 | 230, 240 | eqtrd 2854 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))) |
242 | 207, 241 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))) |
243 | 242 | eqeq2d 2830 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) ↔ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)))) |
244 | 243 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) ↔ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)))) |
245 | | f1of1 6607 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
246 | 49, 245 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
247 | 246 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
248 | 1 | nncnd 11646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
249 | | npcan1 11057 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
251 | 164 | nn0zd 12077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
252 | | uzid 12250 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
253 | 251, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
254 | | peano2uz 12293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
256 | 250, 255 | eqeltrrd 2912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) |
257 | | fzss2 12939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ_{≥}‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
259 | 258 | sselda 3965 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...𝑁)) |
260 | | fzp1elp1 12952 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^{nd}
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
261 | 260 | adantl 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...((𝑁
− 1) + 1))) |
262 | 250 | oveq2d 7164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
263 | 262 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
264 | 261, 263 | eleqtrd 2913 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...𝑁)) |
265 | | f1veqaeq 7007 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ ((2^{nd} ‘𝑇) ∈ (1...𝑁) ∧ ((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁))) → (((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) → (2^{nd}
‘𝑇) =
((2^{nd} ‘𝑇)
+ 1))) |
266 | 247, 259,
264, 265 | syl12anc 834 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) → (2^{nd}
‘𝑇) =
((2^{nd} ‘𝑇)
+ 1))) |
267 | 244, 266 | sylbid 242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))‘(2^{nd} ‘𝑇)) → (2^{nd} ‘𝑇) = ((2^{nd}
‘𝑇) +
1))) |
268 | 211, 267 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘(1^{st} ‘𝑇)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})))) →
(2^{nd} ‘𝑇) =
((2^{nd} ‘𝑇)
+ 1))) |
269 | 268 | necon3d 3035 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
≠ ((2^{nd} ‘𝑇) + 1) → (2^{nd}
‘(1^{st} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))))) |
270 | 210, 269 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))) |
271 | | 2fveq3 6668 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
272 | 271 | neeq1d 3073 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑧)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))) ↔ (2^{nd} ‘(1^{st} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))))) |
273 | 270, 272 | syl5ibrcom 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝑧 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})))))) |
274 | 273 | necon2d 3037 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})))) →
𝑧 ≠ 𝑇)) |
275 | 205, 274 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((((1^{st} ‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
276 | 275 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
277 | 204, 276 | impbid 214 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
278 | | eqop 7723 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩ ↔ ((1^{st} ‘𝑧) = ⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩
∧ (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)))) |
279 | | eqop 7723 |
. . . . . . . . . 10
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((1^{st} ‘𝑧) = ⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩
↔ ((1^{st} ‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))))) |
280 | 75, 279 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → ((1^{st} ‘𝑧) = ⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩
↔ ((1^{st} ‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))))) |
281 | 280 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (((1^{st} ‘𝑧) = ⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩
∧ (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) ↔ (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
282 | 278, 281 | bitrd 281 |
. . . . . . 7
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩ ↔ (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
283 | 74, 282 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ 𝑆 → (𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩ ↔ (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
284 | 283 | adantl 484 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩ ↔ (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))) |
285 | 277, 284 | bitr4d 284 |
. . . 4
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩)) |
286 | 285 | ralrimiva 3180 |
. . 3
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩)) |
287 | | reu6i 3717 |
. . 3
⊢
((⟨⟨(1^{st} ‘(1^{st} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩} ∪ ( I ↾
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}))))⟩, (2^{nd} ‘𝑇)⟩ ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^{st}
‘(1^{st} ‘𝑇)), ((2^{nd} ‘(1^{st}
‘𝑇)) ∘
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))))⟩,
(2^{nd} ‘𝑇)⟩)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
288 | 9, 286, 287 | syl2anc 586 |
. 2
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
289 | | xp2nd 7714 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑇) ∈ (0...𝑁)) |
290 | 32, 289 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈ (0...𝑁)) |
291 | 290 | biantrurd 535 |
. . . . 5
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
∈ (0...𝑁) ∧ ¬
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))))) |
292 | 1 | nnnn0d 11947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ_{0}) |
293 | | nn0uz 12272 |
. . . . . . . . . . . 12
⊢
ℕ_{0} = (ℤ_{≥}‘0) |
294 | 292, 293 | eleqtrdi 2921 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘0)) |
295 | | fzpred 12947 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ_{≥}‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
296 | 294, 295 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
297 | 123 | oveq1i 7158 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
298 | 297 | uneq2i 4134 |
. . . . . . . . . 10
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
299 | 296, 298 | syl6eq 2870 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁))) |
300 | 299 | difeq1d 4096 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1)))) |
301 | | difundir 4255 |
. . . . . . . . . 10
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
302 | | 0lt1 11154 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
303 | | 0re 10635 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
304 | | 1re 10633 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
305 | 303, 304 | ltnlei 10753 |
. . . . . . . . . . . . . 14
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
306 | 302, 305 | mpbi 232 |
. . . . . . . . . . . . 13
⊢ ¬ 1
≤ 0 |
307 | | elfzle1 12902 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
1 ≤ 0) |
308 | 306, 307 | mto 199 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
309 | | incom 4176 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {0}) = ({0} ∩ (1...(𝑁 − 1))) |
310 | 309 | eqeq1i 2824 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅) |
311 | | disjsn 4639 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1))) |
312 | | disj3 4401 |
. . . . . . . . . . . . 13
⊢ (({0}
∩ (1...(𝑁 − 1)))
= ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
313 | 310, 311,
312 | 3bitr3i 303 |
. . . . . . . . . . . 12
⊢ (¬ 0
∈ (1...(𝑁 − 1))
↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
314 | 308, 313 | mpbi 232 |
. . . . . . . . . . 11
⊢ {0} =
({0} ∖ (1...(𝑁
− 1))) |
315 | 314 | uneq1i 4133 |
. . . . . . . . . 10
⊢ ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 − 1)))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
316 | 301, 315 | eqtr4i 2845 |
. . . . . . . . 9
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) = ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 −
1)))) |
317 | | difundir 4255 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
(((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
318 | | difid 4328 |
. . . . . . . . . . . . 13
⊢
((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) = ∅ |
319 | 318 | uneq1i 4133 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(∅ ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
320 | | uncom 4127 |
. . . . . . . . . . . . 13
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(({𝑁} ∖ (1...(𝑁 − 1))) ∪
∅) |
321 | | un0 4342 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) =
({𝑁} ∖ (1...(𝑁 − 1))) |
322 | 320, 321 | eqtri 2842 |
. . . . . . . . . . . 12
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
323 | 317, 319,
322 | 3eqtri 2846 |
. . . . . . . . . . 11
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
324 | | nnuz 12273 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ_{≥}‘1) |
325 | 1, 324 | eleqtrdi 2921 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘1)) |
326 | 250, 325 | eqeltrd 2911 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1)) |
327 | | fzsplit2 12924 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1) ∧ 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
328 | 326, 256,
327 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
329 | 250 | oveq1d 7163 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
330 | 1 | nnzd 12078 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
331 | | fzsn 12941 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
332 | 330, 331 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
333 | 329, 332 | eqtrd 2854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
334 | 333 | uneq2d 4137 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
335 | 328, 334 | eqtrd 2854 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
336 | 335 | difeq1d 4096 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1)))) |
337 | 1 | nnred 11645 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
338 | 337 | ltm1d 11564 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
339 | 164 | nn0red 11948 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
340 | 339, 337 | ltnled 10779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
341 | 338, 340 | mpbid 234 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
342 | | elfzle2 12903 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
343 | 341, 342 | nsyl 142 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
344 | | incom 4176 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1))) |
345 | 344 | eqeq1i 2824 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ({𝑁} ∩
(1...(𝑁 − 1))) =
∅) |
346 | | disjsn 4639 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
347 | | disj3 4401 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
348 | 345, 346,
347 | 3bitr3i 303 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
349 | 343, 348 | sylib 220 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
350 | 323, 336,
349 | 3eqtr4a 2880 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁}) |
351 | 350 | uneq2d 4137 |
. . . . . . . . 9
⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪
{𝑁})) |
352 | 316, 351 | syl5eq 2866 |
. . . . . . . 8
⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪
{𝑁})) |
353 | 300, 352 | eqtrd 2854 |
. . . . . . 7
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁})) |
354 | 353 | eleq2d 2896 |
. . . . . 6
⊢ (𝜑 → ((2^{nd}
‘𝑇) ∈
((0...𝑁) ∖
(1...(𝑁 − 1))) ↔
(2^{nd} ‘𝑇)
∈ ({0} ∪ {𝑁}))) |
355 | | eldif 3944 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
356 | | elun 4123 |
. . . . . . 7
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) ∈ {0} ∨
(2^{nd} ‘𝑇)
∈ {𝑁})) |
357 | 215 | elsn 4574 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {0} ↔ (2^{nd}
‘𝑇) =
0) |
358 | 215 | elsn 4574 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {𝑁} ↔ (2^{nd} ‘𝑇) = 𝑁) |
359 | 357, 358 | orbi12i 910 |
. . . . . . 7
⊢
(((2^{nd} ‘𝑇) ∈ {0} ∨ (2^{nd}
‘𝑇) ∈ {𝑁}) ↔ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) |
360 | 356, 359 | bitri 277 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) = 0 ∨ (2^{nd}
‘𝑇) = 𝑁)) |
361 | 354, 355,
360 | 3bitr3g 315 |
. . . . 5
⊢ (𝜑 → (((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
362 | 291, 361 | bitrd 281 |
. . . 4
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
363 | 362 | biimpa 479 |
. . 3
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁)) |
364 | 1 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑁 ∈
ℕ) |
365 | 4 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{m} (1...𝑁))) |
366 | 6 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑇 ∈ 𝑆) |
367 | | poimirlem22.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
368 | 367 | adantlr 713 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
369 | | simpr 487 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
(2^{nd} ‘𝑇) =
0) |
370 | 364, 3, 365, 366, 368, 369 | poimirlem18 34902 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
371 | 1 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑁 ∈ ℕ) |
372 | 4 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{m} (1...𝑁))) |
373 | 6 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆) |
374 | | poimirlem22.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
375 | 374 | adantlr 713 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
376 | | simpr 487 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → (2^{nd}
‘𝑇) = 𝑁) |
377 | 371, 3, 372, 373, 375, 376 | poimirlem21 34905 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
378 | 370, 377 | jaodan 953 |
. . 3
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
379 | 363, 378 | syldan 593 |
. 2
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
380 | 288, 379 | pm2.61dan 811 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |