Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | adantr 479 |
. . . 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 479 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
6 | | poimirlem22.2 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
7 | 6 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ 𝑆) |
8 | | simpr 475 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
9 | 2, 3, 5, 7, 8 | poimirlem15 32390 |
. . 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 6088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑇)) |
11 | 10 | breq2d 4589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑇))) |
12 | 11 | ifbid 4057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1))) |
13 | 12 | csbeq1d 3505 |
. . . . . . . . . . . . . . . . . . . . 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 6088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (1^{st} ‘𝑡) = (1^{st} ‘𝑇)) |
15 | 14 | fveq2d 6092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑇))) |
16 | 14 | fveq2d 6092 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
17 | 16 | imaeq1d 5371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑗))) |
18 | 17 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1})) |
19 | 16 | imaeq1d 5371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
20 | 19 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
21 | 18, 20 | uneq12d 3729 |
. . . . . . . . . . . . . . . . . . . . . . 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 6545 |
. . . . . . . . . . . . . . . . . . . . . 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 3943 |
. . . . . . . . . . . . . . . . . . . . 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 2643 |
. . . . . . . . . . . . . . . . . . . 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 4667 |
. . . . . . . . . . . . . . . . . . 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 2619 |
. . . . . . . . . . . . . . . . . 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 3332 |
. . . . . . . . . . . . . . . . 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 478 |
. . . . . . . . . . . . . . . 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 479 |
. . . . . . . . . . . . . 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 3327 |
. . . . . . . . . . . . . . . . . . . . 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 2705 |
. . . . . . . . . . . . . . . . . . . 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 7066 |
. . . . . . . . . . . . . . . . . . 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 7066 |
. . . . . . . . . . . . . . . . . 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 7742 |
. . . . . . . . . . . . . . . . 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 12294 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
41 | 40 | ssriv 3571 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
42 | | fss 5955 |
. . . . . . . . . . . . . . . 16
⊢
(((1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
43 | 39, 41, 42 | sylancl 692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
44 | 43 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘(1^{st} ‘𝑇)):(1...𝑁)⟶ℤ) |
45 | | xp2nd 7067 |
. . . . . . . . . . . . . . . . 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 6098 |
. . . . . . . . . . . . . . . . 17
⊢
(2^{nd} ‘(1^{st} ‘𝑇)) ∈ V |
48 | | f1oeq1 6025 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
49 | 47, 48 | elab 3318 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
50 | 46, 49 | sylib 206 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
51 | 50 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
52 | 2, 30, 44, 51, 8 | poimirlem1 32376 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
53 | 52 | adantr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
54 | 1 | ad3antrrr 761 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) → 𝑁 ∈
ℕ) |
55 | | fveq2 6088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑧)) |
56 | 55 | breq2d 4589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑧))) |
57 | 56 | ifbid 4057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1))) |
58 | 57 | csbeq1d 3505 |
. . . . . . . . . . . . . . . . . . . . 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 6088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (1^{st} ‘𝑡) = (1^{st} ‘𝑧)) |
60 | 59 | fveq2d 6092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑧))) |
61 | 59 | fveq2d 6092 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑧 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑧))) |
62 | 61 | imaeq1d 5371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑗))) |
63 | 62 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1})) |
64 | 61 | imaeq1d 5371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
65 | 64 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
66 | 63, 65 | uneq12d 3729 |
. . . . . . . . . . . . . . . . . . . . . . 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 6545 |
. . . . . . . . . . . . . . . . . . . . . 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 3943 |
. . . . . . . . . . . . . . . . . . . . 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 2643 |
. . . . . . . . . . . . . . . . . . . 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 4667 |
. . . . . . . . . . . . . . . . . . 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 2619 |
. . . . . . . . . . . . . . . . . 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 3332 |
. . . . . . . . . . . . . . . . 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 478 |
. . . . . . . . . . . . . . . 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 758 |
. . . . . . . . . . . . . . 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 3327 |
. . . . . . . . . . . . . . . . . . . . 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 2705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
77 | | xp1st 7066 |
. . . . . . . . . . . . . . . . . . . 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 7066 |
. . . . . . . . . . . . . . . . . . 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 7742 |
. . . . . . . . . . . . . . . . . 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 5955 |
. . . . . . . . . . . . . . . . 17
⊢
(((1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
84 | 82, 41, 83 | sylancl 692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
85 | 84 | ad2antlr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶ℤ) |
86 | | xp2nd 7067 |
. . . . . . . . . . . . . . . . . 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 6098 |
. . . . . . . . . . . . . . . . . 18
⊢
(2^{nd} ‘(1^{st} ‘𝑧)) ∈ V |
89 | | f1oeq1 6025 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
90 | 88, 89 | elab 3318 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
91 | 87, 90 | sylib 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2^{nd}
‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
92 | 91 | ad2antlr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘(1^{st} ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
93 | | simpllr 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))) |
94 | | xp2nd 7067 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
95 | 76, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
96 | 95 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2^{nd} ‘𝑧) ∈ (0...𝑁)) |
97 | | eldifsn 4259 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑧) ∈ ((0...𝑁) ∖ {(2^{nd} ‘𝑇)}) ↔ ((2^{nd}
‘𝑧) ∈ (0...𝑁) ∧ (2^{nd}
‘𝑧) ≠
(2^{nd} ‘𝑇))) |
98 | 97 | biimpri 216 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘𝑧) ∈ (0...𝑁) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
99 | 96, 98 | sylan 486 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ ((0...𝑁) ∖
{(2^{nd} ‘𝑇)})) |
100 | 54, 74, 85, 92, 93, 99 | poimirlem2 32377 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇)) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛)) |
101 | 100 | ex 448 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd} ‘𝑧) ≠ (2^{nd}
‘𝑇) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^{nd} ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^{nd} ‘𝑇))‘𝑛))) |
102 | 101 | necon1bd 2799 |
. . . . . . . . . . . 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 2675 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑧) = (2^{nd} ‘𝑇) → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
105 | 104 | biimparc 502 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) →
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1))) |
106 | 105 | anim2i 590 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇)))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
107 | 106 | anassrs 677 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
→ (𝜑 ∧
(2^{nd} ‘𝑧)
∈ (1...(𝑁 −
1)))) |
108 | 73 | adantl 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}))))) |
109 | | breq1 4580 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → (𝑦 < (2^{nd} ‘𝑧) ↔ 0 < (2^{nd}
‘𝑧))) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → 𝑦 = 0) |
111 | 109, 110 | ifbieq1d 4058 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0 → if(𝑦 < (2^{nd}
‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1))) |
112 | | elfznn 12196 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑧) ∈
ℕ) |
113 | 112 | nngt0d 10911 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^{nd}
‘𝑧)) |
114 | 113 | iftrued 4043 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 <
(2^{nd} ‘𝑧),
0, (𝑦 + 1)) =
0) |
115 | 114 | ad2antlr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → if(0 < (2^{nd}
‘𝑧), 0, (𝑦 + 1)) = 0) |
116 | 111, 115 | sylan9eqr 2665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^{nd} ‘𝑧), 𝑦, (𝑦 + 1)) = 0) |
117 | 116 | csbeq1d 3505 |
. . . . . . . . . . . . . . 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 9890 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
119 | | oveq2 6535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
120 | | fz10 12188 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1...0) =
∅ |
121 | 119, 120 | syl6eq 2659 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
122 | 121 | imaeq2d 5372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
∅)) |
123 | 122 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ ∅) ×
{1})) |
124 | | oveq1 6534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
125 | | 0p1e1 10979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
126 | 124, 125 | syl6eq 2659 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
127 | 126 | oveq1d 6542 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
128 | 127 | imaeq2d 5372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑧)) “
(1...𝑁))) |
129 | 128 | xpeq1d 5052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
130 | 123, 129 | uneq12d 3729 |
. . . . . . . . . . . . . . . . . . . 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 5387 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) =
∅ |
132 | 131 | xpeq1i 5049 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) = (∅
× {1}) |
133 | | 0xp 5112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
× {1}) = ∅ |
134 | 132, 133 | eqtri 2631 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) =
∅ |
135 | 134 | uneq1i 3724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
136 | | uncom 3718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∪ (((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪
∅) |
137 | | un0 3918 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
138 | 135, 136,
137 | 3eqtri 2635 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2^{nd} ‘(1^{st} ‘𝑧)) “ ∅) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) |
139 | 130, 138 | syl6eq 2659 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → ((((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) |
140 | 139 | oveq2d 6543 |
. . . . . . . . . . . . . . . . . 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 3524 |
. . . . . . . . . . . . . . . . 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 6042 |
. . . . . . . . . . . . . . . . . . . . . 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 6018 |
. . . . . . . . . . . . . . . . . . . . 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 5052 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (((2^{nd}
‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
147 | 146 | oveq2d 6543 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} + ((1...𝑁) ×
{0}))) |
148 | | ovex 6555 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ∈
V |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V) |
150 | | ffn 5944 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1^{st} ‘(1^{st} ‘𝑧)):(1...𝑁)⟶(0..^𝐾) → (1^{st}
‘(1^{st} ‘𝑧)) Fn (1...𝑁)) |
151 | 82, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1^{st}
‘(1^{st} ‘𝑧)) Fn (1...𝑁)) |
152 | | fnconstg 5991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
153 | 118, 152 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
154 | | eqidd 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) = ((1^{st} ‘(1^{st}
‘𝑧))‘𝑛)) |
155 | 118 | fvconst2 6352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
156 | 155 | adantl 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
157 | 82 | ffvelrnda 6252 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾)) |
158 | | elfzonn0 12335 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1^{st} ‘(1^{st} ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈
ℕ_{0}) |
160 | 159 | nn0cnd 11200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) ∈ ℂ) |
161 | 160 | addid1d 10087 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑧))‘𝑛) + 0) = ((1^{st}
‘(1^{st} ‘𝑧))‘𝑛)) |
162 | 149, 151,
153, 151, 154, 156, 161 | offveq 6793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} + ((1...𝑁) × {0})) =
(1^{st} ‘(1^{st} ‘𝑧))) |
163 | 147, 162 | eqtrd 2643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → ((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
(((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑁)) × {0})) = (1^{st}
‘(1^{st} ‘𝑧))) |
164 | 141, 163 | syl5eq 2655 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑧)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^{st}
‘(1^{st} ‘𝑧))) |
165 | 164 | ad2antlr 758 |
. . . . . . . . . . . . . . 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} ‘𝑧))) |
166 | 117, 165 | eqtrd 2643 |
. . . . . . . . . . . . . 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} ‘𝑧))) |
167 | | nnm1nn0 11181 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ_{0}) |
168 | 1, 167 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ_{0}) |
169 | | 0elfz 12260 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈
ℕ_{0} → 0 ∈ (0...(𝑁 − 1))) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
171 | 170 | ad2antrr 757 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1))) |
172 | | fvex 6098 |
. . . . . . . . . . . . . . 15
⊢
(1^{st} ‘(1^{st} ‘𝑧)) ∈ V |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) ∈ V) |
174 | 108, 166,
171, 173 | fvmptd 6182 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
175 | 107, 174 | sylan 486 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2^{nd} ‘𝑧) =
(2^{nd} ‘𝑇))
∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
176 | 175 | an32s 841 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
177 | 103, 176 | mpdan 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) |
178 | | fveq2 6088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
179 | 178 | eleq1d 2671 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → ((2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
180 | 179 | anbi2d 735 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))))) |
181 | | fveq2 6088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (1^{st} ‘𝑧) = (1^{st} ‘𝑇)) |
182 | 181 | fveq2d 6092 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
183 | 182 | eqeq2d 2619 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)) ↔ (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
184 | 180, 183 | imbi12d 332 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧))) ↔ ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))))) |
185 | 174 | expcom 449 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑧)))) |
186 | 184, 185 | vtoclga 3244 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇)))) |
187 | 7, 186 | mpcom 37 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝐹‘0) =
(1^{st} ‘(1^{st} ‘𝑇))) |
188 | 187 | adantr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1^{st}
‘(1^{st} ‘𝑇))) |
189 | 177, 188 | eqtr3d 2645 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
190 | 189 | adantr 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇))) |
191 | 1 | ad3antrrr 761 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ) |
192 | 6 | ad3antrrr 761 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆) |
193 | | simpllr 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1))) |
194 | | simplr 787 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆) |
195 | 35 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1^{st} ‘𝑇)
∈ (((0..^𝐾)
↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
196 | | xpopth 7075 |
. . . . . . . . . . . . . 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} ‘𝑇))) |
197 | 78, 195, 196 | syl2anr 493 |
. . . . . . . . . . . . 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} ‘𝑇))) |
198 | 33 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
199 | | xpopth 7075 |
. . . . . . . . . . . . . . . 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}
‘𝑇)) ↔ 𝑧 = 𝑇)) |
200 | 199 | biimpd 217 |
. . . . . . . . . . . . . . 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}
‘𝑇)) → 𝑧 = 𝑇)) |
201 | 76, 198, 200 | syl2anr 493 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st} ‘𝑧) = (1^{st} ‘𝑇) ∧ (2^{nd}
‘𝑧) = (2^{nd}
‘𝑇)) → 𝑧 = 𝑇)) |
202 | 103, 201 | mpan2d 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((1^{st} ‘𝑧) = (1^{st} ‘𝑇) → 𝑧 = 𝑇)) |
203 | 197, 202 | sylbid 228 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1^{st}
‘(1^{st} ‘𝑧)) = (1^{st} ‘(1^{st}
‘𝑇)) ∧
(2^{nd} ‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) → 𝑧 = 𝑇)) |
204 | 189, 203 | mpand 706 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇)) → 𝑧 = 𝑇)) |
205 | 204 | necon3d 2802 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇)))) |
206 | 205 | imp 443 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd}
‘(1^{st} ‘𝑧)) ≠ (2^{nd}
‘(1^{st} ‘𝑇))) |
207 | 191, 3, 192, 193, 194, 206 | poimirlem9 32384 |
. . . . . . . 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)}))))) |
208 | 103 | adantr 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^{nd} ‘𝑧) = (2^{nd} ‘𝑇)) |
209 | 190, 207,
208 | jca31 554 |
. . . . . . 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} ‘𝑇))) |
210 | 209 | ex 448 |
. . . . . 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} ‘𝑇)))) |
211 | | simplr 787 |
. . . . . . . 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)}))))) |
212 | | elfznn 12196 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℕ) |
213 | 212 | nnred 10882 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℝ) |
214 | 213 | ltp1d 10803 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
215 | 213, 214 | ltned 10024 |
. . . . . . . . . . . 12
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
216 | 215 | adantl 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
≠ ((2^{nd} ‘𝑇) + 1)) |
217 | | fveq1 6087 |
. . . . . . . . . . . . 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} ‘𝑇))) |
218 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ∈
ℝ) |
219 | | ltp1 10710 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
220 | 218, 219 | ltned 10024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
221 | | fvex 6098 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2^{nd} ‘𝑇) ∈ V |
222 | | ovex 6555 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑇) + 1) ∈ V |
223 | 221, 222,
222, 221 | fpr 6304 |
. . . . . . . . . . . . . . . . . . . . 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} ‘𝑇)}) |
224 | 220, 223 | 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} ‘𝑇)}) |
225 | | f1oi 6071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
226 | | f1of 6035 |
. . . . . . . . . . . . . . . . . . . . 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)})) |
227 | 225, 226 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
228 | | disjdif 3991 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) =
∅ |
229 | | fun 5965 |
. . . . . . . . . . . . . . . . . . . . 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)}))) |
230 | 228, 229 | mpan2 702 |
. . . . . . . . . . . . . . . . . . . 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)}))) |
231 | 224, 227,
230 | sylancl 692 |
. . . . . . . . . . . . . . . . . . 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)}))) |
232 | 221 | prid1 4240 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} |
233 | | elun1 3741 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} → (2^{nd}
‘𝑇) ∈
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
234 | 232, 233 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2^{nd} ‘𝑇) ∈ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})) |
235 | | fvco3 6170 |
. . . . . . . . . . . . . . . . . . 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} ‘𝑇)))) |
236 | 231, 234,
235 | sylancl 692 |
. . . . . . . . . . . . . . . . . 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} ‘𝑇)))) |
237 | | ffn 5944 |
. . . . . . . . . . . . . . . . . . . . . 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)}) |
238 | 224, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} Fn {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
239 | | fnresi 5908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( I
↾ ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) |
240 | 228, 232 | pm3.2i 469 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ∅ ∧
(2^{nd} ‘𝑇)
∈ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
241 | | fvun1 6164 |
. . . . . . . . . . . . . . . . . . . . . 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}
‘𝑇))) |
242 | 239, 240,
241 | mp3an23 1407 |
. . . . . . . . . . . . . . . . . . . . 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}
‘𝑇))) |
243 | 238, 242 | 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}
‘𝑇))) |
244 | 221, 222 | fvpr1 6339 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
245 | 220, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2^{nd} ‘𝑇) ∈ ℝ →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘𝑇) +
1)) |
246 | 243, 245 | eqtrd 2643 |
. . . . . . . . . . . . . . . . . . 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)) |
247 | 246 | fveq2d 6092 |
. . . . . . . . . . . . . . . . . 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))) |
248 | 236, 247 | eqtrd 2643 |
. . . . . . . . . . . . . . . . 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))) |
249 | 213, 248 | 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))) |
250 | 249 | eqeq2d 2619 |
. . . . . . . . . . . . . . 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)))) |
251 | 250 | adantl 480 |
. . . . . . . . . . . . . 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)))) |
252 | | f1of1 6034 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
253 | 50, 252 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
254 | 253 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
255 | 1 | nncnd 10883 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
256 | | npcan1 10306 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
257 | 255, 256 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
258 | 168 | nn0zd 11312 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
259 | | uzid 11534 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
261 | | peano2uz 11573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
262 | 260, 261 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
263 | 257, 262 | eqeltrrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) |
264 | | fzss2 12207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ_{≥}‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
265 | 263, 264 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
266 | 265 | sselda 3567 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2^{nd} ‘𝑇)
∈ (1...𝑁)) |
267 | | fzp1elp1 12219 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^{nd}
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
268 | 267 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...((𝑁
− 1) + 1))) |
269 | 257 | oveq2d 6543 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
270 | 269 | adantr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
271 | 268, 270 | eleqtrd 2689 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
+ 1) ∈ (1...𝑁)) |
272 | | f1veqaeq 6396 |
. . . . . . . . . . . . . . 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))) |
273 | 254, 266,
271, 272 | syl12anc 1315 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) → (2^{nd}
‘𝑇) =
((2^{nd} ‘𝑇)
+ 1))) |
274 | 251, 273 | sylbid 228 |
. . . . . . . . . . . . 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))) |
275 | 217, 274 | syl5 33 |
. . . . . . . . . . . 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))) |
276 | 275 | necon3d 2802 |
. . . . . . . . . . 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)})))))) |
277 | 216, 276 | 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)}))))) |
278 | 181 | fveq2d 6092 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑧)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
279 | 278 | neeq1d 2840 |
. . . . . . . . . 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)})))))) |
280 | 277, 279 | syl5ibrcom 235 |
. . . . . . . . 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)})))))) |
281 | 280 | necon2d 2804 |
. . . . . . . 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)})))) →
𝑧 ≠ 𝑇)) |
282 | 211, 281 | syl5 33 |
. . . . . . 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} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
283 | 282 | adantr 479 |
. . . . . 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} ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
284 | 210, 283 | impbid 200 |
. . . . 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} ‘𝑇)))) |
285 | | eqop 7076 |
. . . . . . . 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} ‘𝑇)))) |
286 | | eqop 7076 |
. . . . . . . . . 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)}))))))) |
287 | 77, 286 | 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)}))))))) |
288 | 287 | anbi1d 736 |
. . . . . . . 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} ‘𝑇)))) |
289 | 285, 288 | bitrd 266 |
. . . . . . 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} ‘𝑇)))) |
290 | 76, 289 | 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} ‘𝑇)))) |
291 | 290 | adantl 480 |
. . . . 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} ‘𝑇)))) |
292 | 284, 291 | bitr4d 269 |
. . . 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} ‘𝑇)⟩)) |
293 | 292 | ralrimiva 2948 |
. . 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} ‘𝑇)⟩)) |
294 | | reu6i 3363 |
. . 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} ‘𝑇)⟩)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
295 | 9, 293, 294 | syl2anc 690 |
. 2
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
296 | | xp2nd 7067 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^{nd} ‘𝑇) ∈ (0...𝑁)) |
297 | 33, 296 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈ (0...𝑁)) |
298 | 297 | biantrurd 527 |
. . . . 5
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
∈ (0...𝑁) ∧ ¬
(2^{nd} ‘𝑇)
∈ (1...(𝑁 −
1))))) |
299 | 1 | nnnn0d 11198 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ_{0}) |
300 | | nn0uz 11554 |
. . . . . . . . . . . 12
⊢
ℕ_{0} = (ℤ_{≥}‘0) |
301 | 299, 300 | syl6eleq 2697 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘0)) |
302 | | fzpred 12214 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ_{≥}‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
303 | 301, 302 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
304 | 125 | oveq1i 6537 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
305 | 304 | uneq2i 3725 |
. . . . . . . . . 10
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
306 | 303, 305 | syl6eq 2659 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁))) |
307 | 306 | difeq1d 3688 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1)))) |
308 | | difundir 3838 |
. . . . . . . . . 10
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
309 | | 0lt1 10399 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
310 | | 0re 9896 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
311 | | 1re 9895 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
312 | 310, 311 | ltnlei 10009 |
. . . . . . . . . . . . . 14
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
313 | 309, 312 | mpbi 218 |
. . . . . . . . . . . . 13
⊢ ¬ 1
≤ 0 |
314 | | elfzle1 12170 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
1 ≤ 0) |
315 | 313, 314 | mto 186 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
316 | | incom 3766 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {0}) = ({0} ∩ (1...(𝑁 − 1))) |
317 | 316 | eqeq1i 2614 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅) |
318 | | disjsn 4191 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1))) |
319 | | disj3 3972 |
. . . . . . . . . . . . 13
⊢ (({0}
∩ (1...(𝑁 − 1)))
= ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
320 | 317, 318,
319 | 3bitr3i 288 |
. . . . . . . . . . . 12
⊢ (¬ 0
∈ (1...(𝑁 − 1))
↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
321 | 315, 320 | mpbi 218 |
. . . . . . . . . . 11
⊢ {0} =
({0} ∖ (1...(𝑁
− 1))) |
322 | 321 | uneq1i 3724 |
. . . . . . . . . 10
⊢ ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 − 1)))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
323 | 308, 322 | eqtr4i 2634 |
. . . . . . . . 9
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) = ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 −
1)))) |
324 | | difundir 3838 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
(((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
325 | | difid 3901 |
. . . . . . . . . . . . 13
⊢
((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) = ∅ |
326 | 325 | uneq1i 3724 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(∅ ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
327 | | uncom 3718 |
. . . . . . . . . . . . 13
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(({𝑁} ∖ (1...(𝑁 − 1))) ∪
∅) |
328 | | un0 3918 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) =
({𝑁} ∖ (1...(𝑁 − 1))) |
329 | 327, 328 | eqtri 2631 |
. . . . . . . . . . . 12
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
330 | 324, 326,
329 | 3eqtri 2635 |
. . . . . . . . . . 11
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
331 | | nnuz 11555 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ_{≥}‘1) |
332 | 1, 331 | syl6eleq 2697 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘1)) |
333 | 257, 332 | eqeltrd 2687 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1)) |
334 | | fzsplit2 12192 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘1) ∧ 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
335 | 333, 263,
334 | syl2anc 690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
336 | 257 | oveq1d 6542 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
337 | 1 | nnzd 11313 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
338 | | fzsn 12209 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
339 | 337, 338 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
340 | 336, 339 | eqtrd 2643 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
341 | 340 | uneq2d 3728 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
342 | 335, 341 | eqtrd 2643 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
343 | 342 | difeq1d 3688 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1)))) |
344 | 1 | nnred 10882 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
345 | 344 | ltm1d 10805 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
346 | 168 | nn0red 11199 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
347 | 346, 344 | ltnled 10035 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
348 | 345, 347 | mpbid 220 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
349 | | elfzle2 12171 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
350 | 348, 349 | nsyl 133 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
351 | | incom 3766 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1))) |
352 | 351 | eqeq1i 2614 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ({𝑁} ∩
(1...(𝑁 − 1))) =
∅) |
353 | | disjsn 4191 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
354 | | disj3 3972 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
355 | 352, 353,
354 | 3bitr3i 288 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
356 | 350, 355 | sylib 206 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
357 | 330, 343,
356 | 3eqtr4a 2669 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁}) |
358 | 357 | uneq2d 3728 |
. . . . . . . . 9
⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪
{𝑁})) |
359 | 323, 358 | syl5eq 2655 |
. . . . . . . 8
⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪
{𝑁})) |
360 | 307, 359 | eqtrd 2643 |
. . . . . . 7
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁})) |
361 | 360 | eleq2d 2672 |
. . . . . 6
⊢ (𝜑 → ((2^{nd}
‘𝑇) ∈
((0...𝑁) ∖
(1...(𝑁 − 1))) ↔
(2^{nd} ‘𝑇)
∈ ({0} ∪ {𝑁}))) |
362 | | eldif 3549 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1)))) |
363 | | elun 3714 |
. . . . . . 7
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) ∈ {0} ∨
(2^{nd} ‘𝑇)
∈ {𝑁})) |
364 | 221 | elsn 4139 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {0} ↔ (2^{nd}
‘𝑇) =
0) |
365 | 221 | elsn 4139 |
. . . . . . . 8
⊢
((2^{nd} ‘𝑇) ∈ {𝑁} ↔ (2^{nd} ‘𝑇) = 𝑁) |
366 | 364, 365 | orbi12i 541 |
. . . . . . 7
⊢
(((2^{nd} ‘𝑇) ∈ {0} ∨ (2^{nd}
‘𝑇) ∈ {𝑁}) ↔ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) |
367 | 363, 366 | bitri 262 |
. . . . . 6
⊢
((2^{nd} ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^{nd} ‘𝑇) = 0 ∨ (2^{nd}
‘𝑇) = 𝑁)) |
368 | 361, 362,
367 | 3bitr3g 300 |
. . . . 5
⊢ (𝜑 → (((2^{nd}
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
369 | 298, 368 | bitrd 266 |
. . . 4
⊢ (𝜑 → (¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁))) |
370 | 369 | biimpa 499 |
. . 3
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2^{nd} ‘𝑇)
= 0 ∨ (2^{nd} ‘𝑇) = 𝑁)) |
371 | 1 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑁 ∈
ℕ) |
372 | 4 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
373 | 6 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) → 𝑇 ∈ 𝑆) |
374 | | poimirlem22.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
375 | 374 | adantlr 746 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
376 | | simpr 475 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
(2^{nd} ‘𝑇) =
0) |
377 | 371, 3, 372, 373, 375, 376 | poimirlem18 32393 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 0) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
378 | 1 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑁 ∈ ℕ) |
379 | 4 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_{𝑚} (1...𝑁))) |
380 | 6 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆) |
381 | | poimirlem22.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
382 | 381 | adantlr 746 |
. . . . 5
⊢ (((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
383 | | simpr 475 |
. . . . 5
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → (2^{nd}
‘𝑇) = 𝑁) |
384 | 378, 3, 379, 380, 382, 383 | poimirlem21 32396 |
. . . 4
⊢ ((𝜑 ∧ (2^{nd}
‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
385 | 377, 384 | jaodan 821 |
. . 3
⊢ ((𝜑 ∧ ((2^{nd}
‘𝑇) = 0 ∨
(2^{nd} ‘𝑇) =
𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
386 | 370, 385 | syldan 485 |
. 2
⊢ ((𝜑 ∧ ¬ (2^{nd}
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
387 | 295, 386 | pm2.61dan 827 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |