Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑁 ∈
ℕ) |
3 | | poimirlem22.s |
. . . 4
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
6 | | poimirlem22.2 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ 𝑆) |
8 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
9 | 2, 3, 5, 7, 8 | poimirlem15 33554 |
. . 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 6229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑇)) |
11 | 10 | breq2d 4697 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑇))) |
12 | 11 | ifbid 4141 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1))) |
13 | 12 | csbeq1d 3573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
14 | | fveq2 6229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (1^{st} ‘𝑡) = (1^{st} ‘𝑇)) |
15 | 14 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑇))) |
16 | 14 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
17 | 16 | imaeq1d 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑗))) |
18 | 17 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1})) |
19 | 16 | imaeq1d 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
20 | 19 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
21 | 18, 20 | uneq12d 3801 |
. . . . . . . . . . . . . . . . . . . . . . 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}))) |
22 | 15, 21 | oveq12d 6708 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → ((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
23 | 22 | csbeq2dv 4025 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
24 | 13, 23 | eqtrd 2685 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
25 | 24 | mpteq2dv 4778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
26 | 25 | eqeq2d 2661 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
27 | 26, 3 | elrab2 3399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
28 | 27 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
29 | 6, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
31 | | elrabi 3391 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
32 | 31, 3 | eleq2s 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
33 | 6, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
34 | | xp1st 7242 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1^{st}
‘𝑇) ∈
(((0..^𝐾)
↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
36 | | xp1st 7242 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
38 | | elmapi 7921 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
40 | | elfzoelz 12509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
41 | 40 | ssriv 3640 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
42 | | fss 6094 |
. . . . . . . . . . . . . . . 16
⊢
(((1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
43 | 39, 41, 42 | sylancl 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
45 | | xp2nd 7243 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
46 | 35, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
47 | | fvex 6239 |
. . . . . . . . . . . . . . . . 17
⊢
(2^{nd} ‘(1^{st} ‘𝑇)) ∈ V |
48 | | f1oeq1 6165 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
49 | 47, 48 | elab 3382 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
50 | 46, 49 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
52 | 2, 30, 44, 51, 8 | poimirlem1 33540 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
53 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
54 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) → 𝑁 ∈
ℕ) |
55 | | fveq2 6229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑧)) |
56 | 55 | breq2d 4697 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑧))) |
57 | 56 | ifbid 4141 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1))) |
58 | 57 | csbeq1d 3573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
59 | | fveq2 6229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (1^{st} ‘𝑡) = (1^{st} ‘𝑧)) |
60 | 59 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑧))) |
61 | 59 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑧 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑧))) |
62 | 61 | imaeq1d 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑗))) |
63 | 62 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1})) |
64 | 61 | imaeq1d 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
65 | 64 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
66 | 63, 65 | uneq12d 3801 |
. . . . . . . . . . . . . . . . . . . . . . 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}))) |
67 | 60, 66 | oveq12d 6708 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
68 | 67 | csbeq2dv 4025 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
69 | 58, 68 | eqtrd 2685 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
70 | 69 | mpteq2dv 4778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
71 | 70 | eqeq2d 2661 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
72 | 71, 3 | elrab2 3399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
73 | 72 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
74 | 73 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
75 | | elrabi 3391 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
76 | 75, 3 | eleq2s 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
77 | | xp1st 7242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
79 | | xp1st 7242 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^{st}
‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
81 | | elmapi 7921 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘(1^{st} ‘𝑧)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
83 | | fss 6094 |
. . . . . . . . . . . . . . . . 17
⊢
(((1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
84 | 82, 41, 83 | sylancl 695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
85 | 84 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
86 | | xp2nd 7243 |
. . . . . . . . . . . . . . . . . 18
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
87 | 78, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
88 | | fvex 6239 |
. . . . . . . . . . . . . . . . . 18
⊢
(2^{nd} ‘(1^{st} ‘𝑧)) ∈ V |
89 | | f1oeq1 6165 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
90 | 88, 89 | elab 3382 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
91 | 87, 90 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
92 | 91 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
93 | | simpllr 815 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
94 | | xp2nd 7243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
95 | 76, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
97 | | eldifsn 4350 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑧) ∈ ((0...𝑁) ∖ {(2^{nd} ‘𝑇)}) ↔ ((2^{nd}
‘𝑧) ∈ (0...𝑁) ∧ (2^{nd}
‘𝑧) ≠
(2^{nd} ‘𝑇))) |
98 | 97 | biimpri 218 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘𝑧) ∈ (0...𝑁) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
99 | 96, 98 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
100 | 54, 74, 85, 92, 93, 99 | poimirlem2 33541 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
101 | 100 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛))) |
102 | 101 | necon1bd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇))) |
103 | 53, 102 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
104 | | eleq1 2718 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑧) = (2^{nd} ‘𝑇) → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
105 | 104 | biimparc 503 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1))) |
106 | 105 | anim2i 592 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
107 | 106 | anassrs 681 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
108 | 73 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
109 | | breq1 4688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → (𝑦 < (2^{nd} ‘𝑧) ↔ 0 < (2^{nd}
‘𝑧))) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → 𝑦 = 0) |
111 | 109, 110 | ifbieq1d 4142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0 → if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1))) |
112 | | elfznn 12408 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑧) ∈
ℕ) |
113 | 112 | nngt0d 11102 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^{nd}
‘𝑧)) |
114 | 113 | iftrued 4127 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 <
(2^{nd} ‘𝑧),
0, (𝑦 + 1)) =
0) |
115 | 114 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1)) = 0) |
116 | 111, 115 | sylan9eqr 2707 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1)) = 0) |
117 | 116 | csbeq1d 3573 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
118 | | c0ex 10072 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
119 | | oveq2 6698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
120 | | fz10 12400 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1...0) =
∅ |
121 | 119, 120 | syl6eq 2701 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
122 | 121 | imaeq2d 5501 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
∅)) |
123 | 122 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ∅) ×
{1})) |
124 | | oveq1 6697 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
125 | | 0p1e1 11170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
126 | 124, 125 | syl6eq 2701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
127 | 126 | oveq1d 6705 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
128 | 127 | imaeq2d 5501 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑁))) |
129 | 128 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
130 | 123, 129 | uneq12d 3801 |
. . . . . . . . . . . . . . . . . . . 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}))) |
131 | | ima0 5516 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) =
∅ |
132 | 131 | xpeq1i 5169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) = (∅
× {1}) |
133 | | 0xp 5233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
× {1}) = ∅ |
134 | 132, 133 | eqtri 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) =
∅ |
135 | 134 | uneq1i 3796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
136 | | uncom 3790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∪ (((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪
∅) |
137 | | un0 4000 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
138 | 135, 136,
137 | 3eqtri 2677 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
139 | 130, 138 | syl6eq 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
140 | 139 | oveq2d 6706 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 0 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}))) |
141 | 118, 140 | csbie 3592 |
. . . . . . . . . . . . . . . . 17
⊢
⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
142 | | f1ofo 6182 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
143 | 91, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
144 | | foima 6158 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
146 | 145 | xpeq1d 5172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
147 | 146 | oveq2d 6706 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} + ((1...𝑁) ×
{0}))) |
148 | | ovexd 6720 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V) |
149 | | ffn 6083 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾) → (1^{st}
‘(1^{st} ‘𝑧)) Fn (1...𝑁)) |
150 | 82, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)) Fn (1...𝑁)) |
151 | | fnconstg 6131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
152 | 118, 151 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
153 | | eqidd 2652 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) = ((1^{st} ‘(1^{st}
‘𝑧))‘𝑛)) |
154 | 118 | fvconst2 6510 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
156 | 82 | ffvelrnda 6399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾)) |
157 | | elfzonn0 12552 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1^{st} ‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
159 | 158 | nn0cnd 11391 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ ℂ) |
160 | 159 | addid1d 10274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) + 0) = ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛)) |
161 | 148, 150,
152, 150, 153, 155, 160 | offveq 6960 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} + ((1...𝑁) × {0})) =
(1^{st} ‘(1^{st} ‘𝑧))) |
162 | 147, 161 | eqtrd 2685 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (1^{st}
‘(1^{st} ‘𝑧))) |
163 | 141, 162 | syl5eq 2697 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
164 | 163 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
165 | 117, 164 | eqtrd 2685 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
166 | | nnm1nn0 11372 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ_{0}) |
167 | 1, 166 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ_{0}) |
168 | | 0elfz 12475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈
ℕ_{0} → 0 ∈ (0...(𝑁 − 1))) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
170 | 169 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1))) |
171 | | fvexd 6241 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) ∈ V) |
172 | 108, 165,
170, 171 | fvmptd 6327 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
173 | 107, 172 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
174 | 173 | an32s 863 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
175 | 103, 174 | mpdan 703 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
176 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
177 | 176 | eleq1d 2715 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
178 | 177 | anbi2d 740 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))))) |
179 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (1^{st} ‘𝑧) = (1^{st} ‘𝑇)) |
180 | 179 | fveq2d 6233 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
181 | 180 | eqeq2d 2661 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)) ↔ (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
182 | 178, 181 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) ↔ ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))))) |
183 | 172 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)))) |
184 | 182, 183 | vtoclga 3303 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
185 | 7, 184 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝐹‘0) =
(1^{st} ‘(1^{st} ‘𝑇))) |
186 | 185 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))) |
187 | 175, 186 | eqtr3d 2687 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
188 | 187 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
189 | 1 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ) |
190 | 6 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆) |
191 | | simpllr 815 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) |
192 | | simplr 807 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆) |
193 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘𝑇)
∈ (((0..^𝐾)
↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
194 | | xpopth 7251 |
. . . . . . . . . . . . . 14
⊢
(((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚}
(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} ‘𝑇))) |
195 | 78, 193, 194 | syl2anr 494 |
. . . . . . . . . . . . 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} ‘𝑇))) |
196 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
197 | | xpopth 7251 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) ↔ 𝑧 = 𝑇)) |
198 | 197 | biimpd 219 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) → 𝑧 = 𝑇)) |
199 | 76, 196, 198 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) → 𝑧 = 𝑇)) |
200 | 103, 199 | mpan2d 710 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((1^{st} ‘𝑧) = (1^{st} ‘𝑇) → 𝑧 = 𝑇)) |
201 | 195, 200 | sylbid 230 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) → 𝑧 = 𝑇)) |
202 | 187, 201 | mpand 711 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇)) → 𝑧 = 𝑇)) |
203 | 202 | necon3d 2844 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇)))) |
204 | 203 | imp 444 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇))) |
205 | 189, 3, 190, 191, 192, 204 | poimirlem9 33548 |
. . . . . . . 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)}))))) |
206 | 103 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
207 | 188, 205,
206 | jca31 556 |
. . . . . . 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} ‘𝑇))) |
208 | 207 | ex 449 |
. . . . . 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} ‘𝑇)))) |
209 | | simplr 807 |
. . . . . . . 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)}))))) |
210 | | elfznn 12408 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℕ) |
211 | 210 | nnred 11073 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℝ) |
212 | 211 | ltp1d 10992 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
213 | 211, 212 | ltned 10211 |
. . . . . . . . . . . 12
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
214 | 213 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
≠ ((2^{nd} ‘𝑇) + 1)) |
215 | | fveq1 6228 |
. . . . . . . . . . . . 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} ‘𝑇))) |
216 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ∈
ℝ) |
217 | | ltp1 10899 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
218 | 216, 217 | ltned 10211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
219 | | fvex 6239 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2^{nd} ‘𝑇) ∈ V |
220 | | ovex 6718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) + 1) ∈ V |
221 | 219, 220,
220, 219 | fpr 6461 |
. . . . . . . . . . . . . . . . . . . . 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} ‘𝑇)}) |
222 | 218, 221 | 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} ‘𝑇)}) |
223 | | f1oi 6212 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
224 | | f1of 6175 |
. . . . . . . . . . . . . . . . . . . . 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)})) |
225 | 223, 224 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
226 | | disjdif 4073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) =
∅ |
227 | | fun 6104 |
. . . . . . . . . . . . . . . . . . . . 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)}))) |
228 | 226, 227 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . 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)}))) |
229 | 222, 225,
228 | sylancl 695 |
. . . . . . . . . . . . . . . . . . 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)}))) |
230 | 219 | prid1 4329 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} |
231 | | elun1 3813 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} → (2^{nd}
‘𝑇) ∈
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
232 | 230, 231 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2^{nd} ‘𝑇) ∈ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})) |
233 | | fvco3 6314 |
. . . . . . . . . . . . . . . . . . 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} ‘𝑇)))) |
234 | 229, 232,
233 | sylancl 695 |
. . . . . . . . . . . . . . . . . 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} ‘𝑇)))) |
235 | | ffn 6083 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}
→ {⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
236 | 222, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
237 | | fnresi 6046 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) |
238 | 226, 230 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ∅ ∧
(2^{nd} ‘𝑇)
∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
239 | | fvun1 6308 |
. . . . . . . . . . . . . . . . . . . . . 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}
‘𝑇))) |
240 | 237, 238,
239 | mp3an23 1456 |
. . . . . . . . . . . . . . . . . . . . 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}
‘𝑇))) |
241 | 236, 240 | 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}
‘𝑇))) |
242 | 219, 220 | fvpr1 6497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
243 | 218, 242 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
244 | 241, 243 | eqtrd 2685 |
. . . . . . . . . . . . . . . . . . 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)) |
245 | 244 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . 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))) |
246 | 234, 245 | eqtrd 2685 |
. . . . . . . . . . . . . . . . 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))) |
247 | 211, 246 | 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))) |
248 | 247 | eqeq2d 2661 |
. . . . . . . . . . . . . . 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)))) |
249 | 248 | adantl 481 |
. . . . . . . . . . . . . 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)))) |
250 | | f1of1 6174 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
251 | 50, 250 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
252 | 251 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
253 | 1 | nncnd 11074 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
254 | | npcan1 10493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
256 | 167 | nn0zd 11518 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
257 | | uzid 11740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
259 | | peano2uz 11779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
261 | 255, 260 | eqeltrrd 2731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) |
262 | | fzss2 12419 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ_{≥}‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
264 | 263 | sselda 3636 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...𝑁)) |
265 | | fzp1elp1 12432 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^{nd}
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
266 | 265 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...((𝑁
− 1) + 1))) |
267 | 255 | oveq2d 6706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
268 | 267 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
269 | 266, 268 | eleqtrd 2732 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...𝑁)) |
270 | | f1veqaeq 6554 |
. . . . . . . . . . . . . . 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))) |
271 | 252, 264,
269, 270 | syl12anc 1364 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) → (2^{nd}
‘𝑇) =
((2^{nd} ‘𝑇)
+ 1))) |
272 | 249, 271 | sylbid 230 |
. . . . . . . . . . . . 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))) |
273 | 215, 272 | 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))) |
274 | 273 | necon3d 2844 |
. . . . . . . . . . 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)})))))) |
275 | 214, 274 | 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)}))))) |
276 | 179 | fveq2d 6233 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
277 | 276 | neeq1d 2882 |
. . . . . . . . . 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)})))))) |
278 | 275, 277 | syl5ibrcom 237 |
. . . . . . . . 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)})))))) |
279 | 278 | necon2d 2846 |
. . . . . . . 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)})))) →
𝑧 ≠ 𝑇)) |
280 | 209, 279 | 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} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
281 | 280 | adantr 480 |
. . . . . 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} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
282 | 208, 281 | impbid 202 |
. . . . 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} ‘𝑇)))) |
283 | | eqop 7252 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(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} ‘𝑇)))) |
284 | | eqop 7252 |
. . . . . . . . . 10
⊢
((1^{st} ‘𝑧) ∈ (((0..^𝐾) ↑_{𝑚} (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)}))))))) |
285 | 77, 284 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(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)}))))))) |
286 | 285 | anbi1d 741 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(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} ‘𝑇)))) |
287 | 283, 286 | bitrd 268 |
. . . . . . 7
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(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} ‘𝑇)))) |
288 | 76, 287 | 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} ‘𝑇)))) |
289 | 288 | adantl 481 |
. . . . 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} ‘𝑇)))) |
290 | 282, 289 | bitr4d 271 |
. . . 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} ‘𝑇)⟩)) |
291 | 290 | ralrimiva 2995 |
. . 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} ‘𝑇)⟩)) |
292 | | reu6i 3430 |
. . 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} ‘𝑇)⟩)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
293 | 9, 291, 292 | syl2anc 694 |
. 2
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
294 | | xp2nd 7243 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑇) ∈ (0...𝑁)) |
295 | 33, 294 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈ (0...𝑁)) |
296 | 295 | biantrurd 528 |
. . . . 5
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
∈ (0...𝑁) ∧ ¬
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))))) |
297 | 1 | nnnn0d 11389 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ_{0}) |
298 | | nn0uz 11760 |
. . . . . . . . . . . 12
⊢
ℕ_{0} = (ℤ_{≥}‘0) |
299 | 297, 298 | syl6eleq 2740 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘0)) |
300 | | fzpred 12427 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ_{≥}‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
301 | 299, 300 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
302 | 125 | oveq1i 6700 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
303 | 302 | uneq2i 3797 |
. . . . . . . . . 10
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
304 | 301, 303 | syl6eq 2701 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁))) |
305 | 304 | difeq1d 3760 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1)))) |
306 | | difundir 3913 |
. . . . . . . . . 10
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
307 | | 0lt1 10588 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
308 | | 0re 10078 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
309 | | 1re 10077 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
310 | 308, 309 | ltnlei 10196 |
. . . . . . . . . . . . . 14
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
311 | 307, 310 | mpbi 220 |
. . . . . . . . . . . . 13
⊢ ¬ 1
≤ 0 |
312 | | elfzle1 12382 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
1 ≤ 0) |
313 | 311, 312 | mto 188 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
314 | | incom 3838 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {0}) = ({0} ∩ (1...(𝑁 − 1))) |
315 | 314 | eqeq1i 2656 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅) |
316 | | disjsn 4278 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1))) |
317 | | disj3 4054 |
. . . . . . . . . . . . 13
⊢ (({0}
∩ (1...(𝑁 − 1)))
= ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
318 | 315, 316,
317 | 3bitr3i 290 |
. . . . . . . . . . . 12
⊢ (¬ 0
∈ (1...(𝑁 − 1))
↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
319 | 313, 318 | mpbi 220 |
. . . . . . . . . . 11
⊢ {0} =
({0} ∖ (1...(𝑁
− 1))) |
320 | 319 | uneq1i 3796 |
. . . . . . . . . 10
⊢ ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 − 1)))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
321 | 306, 320 | eqtr4i 2676 |
. . . . . . . . 9
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) = ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 −
1)))) |
322 | | difundir 3913 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
(((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
323 | | difid 3981 |
. . . . . . . . . . . . 13
⊢
((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) = ∅ |
324 | 323 | uneq1i 3796 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(∅ ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
325 | | uncom 3790 |
. . . . . . . . . . . . 13
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(({𝑁} ∖ (1...(𝑁 − 1))) ∪
∅) |
326 | | un0 4000 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) =
({𝑁} ∖ (1...(𝑁 − 1))) |
327 | 325, 326 | eqtri 2673 |
. . . . . . . . . . . 12
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
328 | 322, 324,
327 | 3eqtri 2677 |
. . . . . . . . . . 11
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
329 | | nnuz 11761 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ_{≥}‘1) |
330 | 1, 329 | syl6eleq 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘1)) |
331 | 255, 330 | eqeltrd 2730 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1)) |
332 | | fzsplit2 12404 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1) ∧ 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
333 | 331, 261,
332 | syl2anc 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
334 | 255 | oveq1d 6705 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
335 | 1 | nnzd 11519 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
336 | | fzsn 12421 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
337 | 335, 336 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
338 | 334, 337 | eqtrd 2685 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
339 | 338 | uneq2d 3800 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
340 | 333, 339 | eqtrd 2685 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
341 | 340 | difeq1d 3760 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1)))) |
342 | 1 | nnred 11073 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
343 | 342 | ltm1d 10994 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
344 | 167 | nn0red 11390 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
345 | 344, 342 | ltnled 10222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
346 | 343, 345 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
347 | | elfzle2 12383 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
348 | 346, 347 | nsyl 135 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
349 | | incom 3838 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1))) |
350 | 349 | eqeq1i 2656 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ({𝑁} ∩
(1...(𝑁 − 1))) =
∅) |
351 | | disjsn 4278 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
352 | | disj3 4054 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
353 | 350, 351,
352 | 3bitr3i 290 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
354 | 348, 353 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
355 | 328, 341,
354 | 3eqtr4a 2711 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁}) |
356 | 355 | uneq2d 3800 |
. . . . . . . . 9
⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪
{𝑁})) |
357 | 321, 356 | syl5eq 2697 |
. . . . . . . 8
⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪
{𝑁})) |
358 | 305, 357 | eqtrd 2685 |
. . . . . . 7
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁})) |
359 | 358 | eleq2d 2716 |
. . . . . 6
⊢ (𝜑 → ((2^{nd}
‘𝑇) ∈
((0...𝑁) ∖
(1...(𝑁 − 1))) ↔
(2^{nd} ‘𝑇)
∈ ({0} ∪ {𝑁}))) |
360 | | eldif 3617 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
361 | | elun 3786 |
. . . . . . 7
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) ∈ {0} ∨
(2^{nd} ‘𝑇)
∈ {𝑁})) |
362 | 219 | elsn 4225 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {0} ↔ (2^{nd}
‘𝑇) =
0) |
363 | 219 | elsn 4225 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {𝑁} ↔ (2^{nd} ‘𝑇) = 𝑁) |
364 | 362, 363 | orbi12i 542 |
. . . . . . 7
⊢
(((2^{nd} ‘𝑇) ∈ {0} ∨ (2^{nd}
‘𝑇) ∈ {𝑁}) ↔ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) |
365 | 361, 364 | bitri 264 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) = 0 ∨ (2^{nd}
‘𝑇) = 𝑁)) |
366 | 359, 360,
365 | 3bitr3g 302 |
. . . . 5
⊢ (𝜑 → (((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
367 | 296, 366 | bitrd 268 |
. . . 4
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
368 | 367 | biimpa 500 |
. . 3
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁)) |
369 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑁 ∈
ℕ) |
370 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
371 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑇 ∈ 𝑆) |
372 | | poimirlem22.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
373 | 372 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
374 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
(2^{nd} ‘𝑇) =
0) |
375 | 369, 3, 370, 371, 373, 374 | poimirlem18 33557 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
376 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑁 ∈ ℕ) |
377 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
378 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆) |
379 | | poimirlem22.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
380 | 379 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
381 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → (2^{nd}
‘𝑇) = 𝑁) |
382 | 376, 3, 377, 378, 380, 381 | poimirlem21 33560 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
383 | 375, 382 | jaodan 843 |
. . 3
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
384 | 368, 383 | syldan 486 |
. 2
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
385 | 293, 384 | pm2.61dan 849 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |