Step | Hyp | Ref
| Expression |
1 | | resundi 5836 |
. . . 4
⊢
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
(((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
2 | | poimir.0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | 2 | nncnd 11645 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
4 | | npcan1 11058 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
6 | 2 | nnzd 12078 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | | peano2zm 12017 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
8 | | uzid 12250 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
9 | | peano2uz 12293 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
10 | 6, 7, 8, 9 | 4syl 19 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ_{≥}‘(𝑁 − 1))) |
11 | 5, 10 | eqeltrrd 2894 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘(𝑁 − 1))) |
12 | | fzss2 12946 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ_{≥}‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
14 | | poimirlem9.2 |
. . . . . . . . 9
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1))) |
15 | 13, 14 | sseldd 3919 |
. . . . . . . 8
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈ (1...𝑁)) |
16 | | fzp1elp1 12959 |
. . . . . . . . . 10
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^{nd}
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((2^{nd}
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
18 | 5 | oveq2d 7155 |
. . . . . . . . 9
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
19 | 17, 18 | eleqtrd 2895 |
. . . . . . . 8
⊢ (𝜑 → ((2^{nd}
‘𝑇) + 1) ∈
(1...𝑁)) |
20 | 15, 19 | prssd 4718 |
. . . . . . 7
⊢ (𝜑 → {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)} ⊆
(1...𝑁)) |
21 | | undif 4391 |
. . . . . . 7
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)})) =
(1...𝑁)) |
22 | 20, 21 | sylib 221 |
. . . . . 6
⊢ (𝜑 → ({(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)} ∪
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) = (1...𝑁)) |
23 | 22 | reseq2d 5822 |
. . . . 5
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ (1...𝑁))) |
24 | | poimirlem9.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
25 | | elrabi 3626 |
. . . . . . . . 9
⊢ (𝑈 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑈 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
26 | | poimirlem22.s |
. . . . . . . . 9
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
27 | 25, 26 | eleq2s 2911 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
28 | | xp1st 7707 |
. . . . . . . 8
⊢ (𝑈 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑈) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
29 | | xp2nd 7708 |
. . . . . . . 8
⊢
((1^{st} ‘𝑈) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
30 | 24, 27, 28, 29 | 4syl 19 |
. . . . . . 7
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
31 | | fvex 6662 |
. . . . . . . 8
⊢
(2^{nd} ‘(1^{st} ‘𝑈)) ∈ V |
32 | | f1oeq1 6583 |
. . . . . . . 8
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))) |
33 | 31, 32 | elab 3618 |
. . . . . . 7
⊢
((2^{nd} ‘(1^{st} ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)) |
34 | 30, 33 | sylib 221 |
. . . . . 6
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)) |
35 | | f1ofn 6595 |
. . . . . 6
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑈)) Fn (1...𝑁)) |
36 | | fnresdm 6442 |
. . . . . 6
⊢
((2^{nd} ‘(1^{st} ‘𝑈)) Fn (1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ (1...𝑁)) = (2^{nd} ‘(1^{st}
‘𝑈))) |
37 | 34, 35, 36 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ (1...𝑁)) = (2^{nd} ‘(1^{st}
‘𝑈))) |
38 | 23, 37 | eqtrd 2836 |
. . . 4
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
(2^{nd} ‘(1^{st} ‘𝑈))) |
39 | 1, 38 | syl5eqr 2850 |
. . 3
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (2^{nd}
‘(1^{st} ‘𝑈))) |
40 | | 2lt3 11801 |
. . . . . 6
⊢ 2 <
3 |
41 | | 2re 11703 |
. . . . . . 7
⊢ 2 ∈
ℝ |
42 | | 3re 11709 |
. . . . . . 7
⊢ 3 ∈
ℝ |
43 | 41, 42 | ltnlei 10754 |
. . . . . 6
⊢ (2 < 3
↔ ¬ 3 ≤ 2) |
44 | 40, 43 | mpbi 233 |
. . . . 5
⊢ ¬ 3
≤ 2 |
45 | | df-pr 4531 |
. . . . . . . . . . . 12
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} = ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩} ∪
{⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) |
46 | 45 | coeq2i 5699 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩} ∪
{⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) |
47 | | coundi 6071 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩} ∪
{⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩})
∪ ((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) |
48 | 46, 47 | eqtri 2824 |
. . . . . . . . . 10
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩})
∪ ((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) |
49 | | poimirlem9.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
50 | | elrabi 3626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{f} + ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
51 | 50, 26 | eleq2s 2911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
52 | | xp1st 7707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
53 | | xp2nd 7708 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{m} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
54 | 49, 51, 52, 53 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
55 | | fvex 6662 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2^{nd} ‘(1^{st} ‘𝑇)) ∈ V |
56 | | f1oeq1 6583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
57 | 55, 56 | elab 3618 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
58 | 54, 57 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
59 | | f1of1 6593 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
61 | 19 | snssd 4705 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {((2^{nd}
‘𝑇) + 1)} ⊆
(1...𝑁)) |
62 | | f1ores 6608 |
. . . . . . . . . . . . . . . . 17
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2^{nd} ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1)})) |
63 | 60, 61, 62 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1)})) |
64 | | f1of 6594 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1)}) → ((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶((2^{nd} ‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1)})) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶((2^{nd} ‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1)})) |
66 | | f1ofn 6595 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
67 | 58, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
68 | | fnsnfv 6722 |
. . . . . . . . . . . . . . . . 17
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ ((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁)) → {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} = ((2^{nd}
‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1)})) |
69 | 67, 19, 68 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} = ((2^{nd}
‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1)})) |
70 | 69 | feq3d 6478 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶((2^{nd} ‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1)}))) |
71 | 65, 70 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
72 | | eqid 2801 |
. . . . . . . . . . . . . . 15
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩} = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)⟩} |
73 | | fvex 6662 |
. . . . . . . . . . . . . . . 16
⊢
(2^{nd} ‘𝑇) ∈ V |
74 | | ovex 7172 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑇) + 1) ∈ V |
75 | 73, 74 | fsn 6878 |
. . . . . . . . . . . . . . 15
⊢
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩}:{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘𝑇) + 1)} ↔
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩} = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)⟩}) |
76 | 72, 75 | mpbir 234 |
. . . . . . . . . . . . . 14
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩}:{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘𝑇) +
1)} |
77 | | fco2 6511 |
. . . . . . . . . . . . . 14
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}):{((2^{nd}
‘𝑇) +
1)}⟶{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩}:{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘𝑇) + 1)}) →
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)⟩}):{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
78 | 71, 76, 77 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)⟩}):{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
79 | | fvex 6662 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ∈
V |
80 | 79 | fconst2 6948 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)⟩}):{(2^{nd} ‘𝑇)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩}) =
({(2^{nd} ‘𝑇)} × {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))})) |
81 | 78, 80 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩}) =
({(2^{nd} ‘𝑇)} × {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))})) |
82 | 73, 79 | xpsn 6884 |
. . . . . . . . . . . 12
⊢
({(2^{nd} ‘𝑇)} × {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) =
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} |
83 | 81, 82 | eqtrdi 2852 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩}) =
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
84 | 83 | uneq1d 4092 |
. . . . . . . . . 10
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩})
∪ ((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) = ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}))) |
85 | 48, 84 | syl5eq 2848 |
. . . . . . . . 9
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) =
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}))) |
86 | | elfznn 12935 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℕ) |
87 | 14, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
ℕ) |
88 | 87 | nnred 11644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
ℝ) |
89 | 88 | ltp1d 11563 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘𝑇) <
((2^{nd} ‘𝑇)
+ 1)) |
90 | 88, 89 | ltned 10769 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2^{nd}
‘𝑇) ≠
((2^{nd} ‘𝑇)
+ 1)) |
91 | 90 | necomd 3045 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘𝑇) + 1) ≠
(2^{nd} ‘𝑇)) |
92 | | f1veqaeq 6997 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ (((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2^{nd}
‘𝑇) ∈ (1...𝑁))) → (((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) → ((2^{nd}
‘𝑇) + 1) =
(2^{nd} ‘𝑇))) |
93 | 60, 19, 15, 92 | syl12anc 835 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) → ((2^{nd}
‘𝑇) + 1) =
(2^{nd} ‘𝑇))) |
94 | 93 | necon3d 3011 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2^{nd}
‘𝑇) + 1) ≠
(2^{nd} ‘𝑇)
→ ((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)))) |
95 | 91, 94 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))) |
96 | 95 | neneqd 2995 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))) |
97 | 73, 79 | opth 5336 |
. . . . . . . . . . . 12
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ↔ ((2^{nd}
‘𝑇) = (2^{nd}
‘𝑇) ∧
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)))) |
98 | 97 | simprbi 500 |
. . . . . . . . . . 11
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ → ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) = ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))) |
99 | 96, 98 | nsyl 142 |
. . . . . . . . . 10
⊢ (𝜑 → ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩) |
100 | 90 | neneqd 2995 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (2^{nd}
‘𝑇) =
((2^{nd} ‘𝑇)
+ 1)) |
101 | 73, 79 | opth1 5335 |
. . . . . . . . . . 11
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ →
(2^{nd} ‘𝑇) =
((2^{nd} ‘𝑇)
+ 1)) |
102 | 100, 101 | nsyl 142 |
. . . . . . . . . 10
⊢ (𝜑 → ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩) |
103 | | opex 5324 |
. . . . . . . . . . . . . . 15
⊢
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
V |
104 | 103 | snid 4564 |
. . . . . . . . . . . . . 14
⊢
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} |
105 | | elun1 4106 |
. . . . . . . . . . . . . 14
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} →
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}))) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) |
107 | | eleq2 2881 |
. . . . . . . . . . . . 13
⊢
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} →
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) ↔ ⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) +
1))⟩})) |
108 | 106, 107 | mpbii 236 |
. . . . . . . . . . . 12
⊢
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} →
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
109 | 103 | elpr 4551 |
. . . . . . . . . . . . 13
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ↔
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∨
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩)) |
110 | | oran 987 |
. . . . . . . . . . . . 13
⊢
((⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∨
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩) ↔ ¬
(¬ ⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∧ ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩)) |
111 | 109, 110 | bitri 278 |
. . . . . . . . . . . 12
⊢
(⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ ∈
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ↔ ¬
(¬ ⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∧ ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩)) |
112 | 108, 111 | sylib 221 |
. . . . . . . . . . 11
⊢
(({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} → ¬
(¬ ⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∧ ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩)) |
113 | 112 | necon2ai 3019 |
. . . . . . . . . 10
⊢ ((¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩ ∧ ¬
⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩ =
⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩) →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) ≠ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
114 | 99, 102, 113 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ({⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∪
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩})) ≠ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
115 | 85, 114 | eqnetrd 3057 |
. . . . . . . 8
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ≠
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
116 | | fnressn 6901 |
. . . . . . . . . . . 12
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ (2^{nd} ‘𝑇) ∈ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇)}) = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩}) |
117 | 67, 15, 116 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇)}) = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩}) |
118 | | fnressn 6901 |
. . . . . . . . . . . 12
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ ((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}) =
{⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
119 | 67, 19, 118 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)}) =
{⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
120 | 117, 119 | uneq12d 4094 |
. . . . . . . . . 10
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)})) =
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩} ∪
{⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) +
1))⟩})) |
121 | | df-pr 4531 |
. . . . . . . . . . . 12
⊢
{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} = ({(2^{nd} ‘𝑇)} ∪ {((2^{nd}
‘𝑇) +
1)}) |
122 | 121 | reseq2i 5819 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ({(2^{nd} ‘𝑇)} ∪ {((2^{nd}
‘𝑇) +
1)})) |
123 | | resundi 5836 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ ({(2^{nd} ‘𝑇)} ∪ {((2^{nd}
‘𝑇) + 1)})) =
(((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)})) |
124 | 122, 123 | eqtri 2824 |
. . . . . . . . . 10
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1)})) |
125 | | df-pr 4531 |
. . . . . . . . . 10
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} =
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩} ∪
{⟨((2^{nd} ‘𝑇) + 1), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
126 | 120, 124,
125 | 3eqtr4g 2861 |
. . . . . . . . 9
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) =
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}) |
127 | | poimirlem9.4 |
. . . . . . . . . . 11
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑈)) ≠ (2^{nd}
‘(1^{st} ‘𝑇))) |
128 | 2, 26, 49, 14, 24 | poimirlem8 35064 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
129 | | uneq12 4088 |
. . . . . . . . . . . . . 14
⊢
((((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) →
(((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
130 | | resundi 5836 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
(((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
131 | 22 | reseq2d 5822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ (1...𝑁))) |
132 | | fnresdm 6442 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ (1...𝑁)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
133 | 58, 66, 132 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ (1...𝑁)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
134 | 131, 133 | eqtrd 2836 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
(2^{nd} ‘(1^{st} ‘𝑇))) |
135 | 130, 134 | syl5eqr 2850 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (2^{nd}
‘(1^{st} ‘𝑇))) |
136 | 39, 135 | eqeq12d 2817 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) ↔
(2^{nd} ‘(1^{st} ‘𝑈)) = (2^{nd} ‘(1^{st}
‘𝑇)))) |
137 | 129, 136 | syl5ib 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) →
(2^{nd} ‘(1^{st} ‘𝑈)) = (2^{nd} ‘(1^{st}
‘𝑇)))) |
138 | 128, 137 | mpan2d 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) → (2^{nd}
‘(1^{st} ‘𝑈)) = (2^{nd} ‘(1^{st}
‘𝑇)))) |
139 | 138 | necon3d 3011 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ≠ (2^{nd}
‘(1^{st} ‘𝑇)) → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
140 | 127, 139 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
141 | 140 | necomd 3045 |
. . . . . . . . 9
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
142 | 126, 141 | eqnetrrd 3058 |
. . . . . . . 8
⊢ (𝜑 → {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ≠
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
143 | | prex 5301 |
. . . . . . . . . . . 12
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ∈ V |
144 | 55, 143 | coex 7621 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ∈
V |
145 | | prex 5301 |
. . . . . . . . . . 11
⊢
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∈
V |
146 | 31 | resex 5870 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∈
V |
147 | | hashtpg 13843 |
. . . . . . . . . . 11
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ∈ V ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∈ V ∧
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∈ V) →
((((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ≠
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ≠
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) ↔
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) =
3)) |
148 | 144, 145,
146, 147 | mp3an 1458 |
. . . . . . . . . 10
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ≠
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ≠
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) ↔
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) = 3) |
149 | 148 | biimpi 219 |
. . . . . . . . 9
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ≠
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ≠
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) = 3) |
150 | 149 | 3expia 1118 |
. . . . . . . 8
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ≠
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ∧
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} ≠
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) →
(((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) =
3)) |
151 | 115, 142,
150 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) =
3)) |
152 | | prex 5301 |
. . . . . . . . . . . . 13
⊢
{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∈ V |
153 | | prex 5301 |
. . . . . . . . . . . . 13
⊢
{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∈ V |
154 | 152, 153 | mapval 8405 |
. . . . . . . . . . . 12
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↑_{m}
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) = {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} |
155 | | prfi 8781 |
. . . . . . . . . . . . 13
⊢
{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∈ Fin |
156 | | prfi 8781 |
. . . . . . . . . . . . 13
⊢
{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∈ Fin |
157 | | mapfi 8808 |
. . . . . . . . . . . . 13
⊢
(({((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∈ Fin ∧
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)} ∈ Fin) → ({((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↑_{m}
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) ∈ Fin) |
158 | 155, 156,
157 | mp2an 691 |
. . . . . . . . . . . 12
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↑_{m}
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) ∈ Fin |
159 | 154, 158 | eqeltrri 2890 |
. . . . . . . . . . 11
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈ Fin |
160 | | f1of 6594 |
. . . . . . . . . . . 12
⊢ (𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} → 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
161 | 160 | ss2abi 3997 |
. . . . . . . . . . 11
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} |
162 | | ssfi 8726 |
. . . . . . . . . . 11
⊢ (({𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) → {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈
Fin) |
163 | 159, 161,
162 | mp2an 691 |
. . . . . . . . . 10
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈ Fin |
164 | 19, 15 | prssd 4718 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}
⊆ (1...𝑁)) |
165 | | f1ores 6608 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)} ⊆
(1...𝑁)) →
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1), (2^{nd} ‘𝑇)})) |
166 | 60, 164, 165 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1), (2^{nd} ‘𝑇)})) |
167 | | fnimapr 6726 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ ((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2^{nd}
‘𝑇) ∈ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) =
{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
168 | 67, 19, 15, 167 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) =
{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
169 | 168 | f1oeq3d 6591 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑇)) “
{((2^{nd} ‘𝑇)
+ 1), (2^{nd} ‘𝑇)}) ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
170 | 166, 169 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
171 | | f1oprg 6638 |
. . . . . . . . . . . . . . 15
⊢
((((2^{nd} ‘𝑇) ∈ V ∧ ((2^{nd}
‘𝑇) + 1) ∈ V)
∧ (((2^{nd} ‘𝑇) + 1) ∈ V ∧ (2^{nd}
‘𝑇) ∈ V)) →
(((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)}–1-1-onto→{((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)})) |
172 | 73, 74, 74, 73, 171 | mp4an 692 |
. . . . . . . . . . . . . 14
⊢
(((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)}–1-1-onto→{((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)}) |
173 | 90, 91, 172 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)}) |
174 | | f1oco 6616 |
. . . . . . . . . . . . 13
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}):{((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∧ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)}) → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}):{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
175 | 170, 173,
174 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}):{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
176 | | rnpropg 6050 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘𝑇) ∈ V ∧ ((2^{nd}
‘𝑇) + 1) ∈ V)
→ ran {⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} = {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) |
177 | 73, 74, 176 | mp2an 691 |
. . . . . . . . . . . . . 14
⊢ ran
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} = {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)} |
178 | 177 | eqimssi 3976 |
. . . . . . . . . . . . 13
⊢ ran
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ⊆ {((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)} |
179 | | cores 6073 |
. . . . . . . . . . . . 13
⊢ (ran
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩} ⊆ {((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)}
→ (((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) |
180 | | f1oeq1 6583 |
. . . . . . . . . . . . 13
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) →
((((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}):{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
181 | 178, 179,
180 | mp2b 10 |
. . . . . . . . . . . 12
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) ↾ {((2^{nd} ‘𝑇) + 1), (2^{nd}
‘𝑇)}) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}):{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
182 | 175, 181 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
183 | 95 | necomd 3045 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))) |
184 | | fvex 6662 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ∈ V |
185 | | f1oprg 6638 |
. . . . . . . . . . . . . 14
⊢
((((2^{nd} ‘𝑇) ∈ V ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ∈ V) ∧
(((2^{nd} ‘𝑇)
+ 1) ∈ V ∧ ((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)) ∈ V))
→ (((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))) →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))})) |
186 | 73, 184, 74, 79, 185 | mp4an 692 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))) →
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
187 | 90, 183, 186 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
188 | | prcom 4631 |
. . . . . . . . . . . . 13
⊢
{((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} = {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} |
189 | | f1oeq3 6585 |
. . . . . . . . . . . . 13
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} = {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} →
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} ↔
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
190 | 188, 189 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
({⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))} ↔
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
191 | 187, 190 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
192 | | f1of1 6593 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–1-1→(1...𝑁)) |
193 | 34, 192 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–1-1→(1...𝑁)) |
194 | | f1ores 6608 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1→(1...𝑁) ∧ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑈)) “
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) |
195 | 193, 20, 194 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑈)) “
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) |
196 | | dff1o3 6600 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑈)))) |
197 | 196 | simprbi 500 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑈))) |
198 | | imadif 6412 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑈)) →
((2^{nd} ‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
199 | 34, 197, 198 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
200 | | f1ofo 6601 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑈)):(1...𝑁)–onto→(1...𝑁)) |
201 | | foima 6574 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) = (1...𝑁)) |
202 | 34, 200, 201 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) = (1...𝑁)) |
203 | | f1ofo 6601 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
204 | | foima 6574 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
205 | 58, 203, 204 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
206 | 202, 205 | eqtr4d 2839 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑁))) |
207 | 128 | rneqd 5776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ran ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
208 | | df-ima 5536 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ran ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
209 | | df-ima 5536 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ran ((2^{nd}
‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
210 | 207, 208,
209 | 3eqtr4g 2861 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
211 | 206, 210 | difeq12d 4054 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
212 | | dff1o3 6600 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑇)))) |
213 | 212 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑇))) |
214 | | imadif 6412 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑇)) →
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
215 | 58, 213, 214 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})))) |
216 | | dfin4 4197 |
. . . . . . . . . . . . . . . . . 18
⊢
((1...𝑁) ∩
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) = ((1...𝑁) ∖
((1...𝑁) ∖
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)})) |
217 | | sseqin2 4145 |
. . . . . . . . . . . . . . . . . . 19
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}) |
218 | 20, 217 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑁) ∩ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}) |
219 | 216, 218 | syl5eqr 2850 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}) |
220 | 219 | imaeq2d 5900 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
221 | 215, 220 | eqtr3d 2838 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
222 | 199, 211,
221 | 3eqtrd 2840 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
223 | 219 | imaeq2d 5900 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = ((2^{nd}
‘(1^{st} ‘𝑈)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
224 | | fnimapr 6726 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ (2^{nd} ‘𝑇) ∈ (1...𝑁) ∧ ((2^{nd} ‘𝑇) + 1) ∈ (1...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
225 | 67, 15, 19, 224 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)), ((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))}) |
226 | 225, 188 | eqtrdi 2852 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
227 | 222, 223,
226 | 3eqtr3d 2844 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) “ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
228 | 227 | f1oeq3d 6591 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→((2^{nd} ‘(1^{st}
‘𝑈)) “
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)}) ↔ ((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
229 | 195, 228 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
230 | | ssabral 3993 |
. . . . . . . . . . . 12
⊢
({((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ↔ ∀𝑓 ∈ {((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) |
231 | | f1oeq1 6583 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) → (𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
232 | | f1oeq1 6583 |
. . . . . . . . . . . . 13
⊢ (𝑓 = {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩} → (𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
233 | | f1oeq1 6583 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) → (𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
234 | 144, 145,
146, 231, 232, 233 | raltp 4604 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
{((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ↔ (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∧ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
235 | 230, 234 | bitri 278 |
. . . . . . . . . . 11
⊢
({((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ↔ (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∧ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∧ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}):{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))})) |
236 | 182, 191,
229, 235 | syl3anbrc 1340 |
. . . . . . . . . 10
⊢ (𝜑 → {((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) |
237 | | hashss 13770 |
. . . . . . . . . 10
⊢ (({𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈ Fin ∧
{((2^{nd} ‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}),
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘(1^{st}
‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) ≤
(♯‘{𝑓 ∣
𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}})) |
238 | 163, 236,
237 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) ≤
(♯‘{𝑓 ∣
𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}})) |
239 | 153 | enref 8529 |
. . . . . . . . . . . 12
⊢
{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)} |
240 | | hashprg 13756 |
. . . . . . . . . . . . . . . 16
⊢
((((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ∈ V ∧
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ∈ V) →
(((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ↔
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) = 2)) |
241 | 79, 184, 240 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)) ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇)) ↔
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) = 2) |
242 | 95, 241 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) = 2) |
243 | | hashprg 13756 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘𝑇) ∈ V ∧ ((2^{nd}
‘𝑇) + 1) ∈ V)
→ ((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) ↔
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = 2)) |
244 | 73, 74, 243 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘𝑇) ≠ ((2^{nd} ‘𝑇) + 1) ↔
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = 2) |
245 | 90, 244 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = 2) |
246 | 242, 245 | eqtr4d 2839 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) =
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
247 | | hashen 13707 |
. . . . . . . . . . . . . 14
⊢
(({((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ∈ Fin ∧
{(2^{nd} ‘𝑇),
((2^{nd} ‘𝑇)
+ 1)} ∈ Fin) → ((♯‘{((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) =
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ↔ {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})) |
248 | 155, 156,
247 | mp2an 691 |
. . . . . . . . . . . . 13
⊢
((♯‘{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘𝑇) + 1)),
((2^{nd} ‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}) =
(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ↔ {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}) |
249 | 246, 248 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → {((2^{nd}
‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}) |
250 | | hashfacen 13812 |
. . . . . . . . . . . 12
⊢
(({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)} ∧
{((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))} ≈ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}) →
{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) |
251 | 239, 249,
250 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) |
252 | 153, 153 | mapval 8405 |
. . . . . . . . . . . . . 14
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ↑_{m} {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}) = {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} |
253 | | mapfi 8808 |
. . . . . . . . . . . . . . 15
⊢
(({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∈ Fin ∧ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)} ∈ Fin)
→ ({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ↑_{m} {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}) ∈
Fin) |
254 | 156, 156,
253 | mp2an 691 |
. . . . . . . . . . . . . 14
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ↑_{m} {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}) ∈
Fin |
255 | 252, 254 | eqeltrri 2890 |
. . . . . . . . . . . . 13
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ∈
Fin |
256 | | f1of 6594 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} → 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) |
257 | 256 | ss2abi 3997 |
. . . . . . . . . . . . 13
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} |
258 | | ssfi 8726 |
. . . . . . . . . . . . 13
⊢ (({𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}⟶{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) → {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ∈ Fin) |
259 | 255, 257,
258 | mp2an 691 |
. . . . . . . . . . . 12
⊢ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ∈ Fin |
260 | | hashen 13707 |
. . . . . . . . . . . 12
⊢ (({𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}} ∈ Fin) →
((♯‘{𝑓 ∣
𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}})) |
261 | 163, 259,
260 | mp2an 691 |
. . . . . . . . . . 11
⊢
((♯‘{𝑓
∣ 𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) |
262 | 251, 261 | sylibr 237 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}})) |
263 | | hashfac 13816 |
. . . . . . . . . . . 12
⊢
({(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)} ∈ Fin →
(♯‘{𝑓 ∣
𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) =
(!‘(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) |
264 | 156, 263 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(♯‘{𝑓
∣ 𝑓:{(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) =
(!‘(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
265 | 245 | fveq2d 6653 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(!‘(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = (!‘2)) |
266 | | fac2 13639 |
. . . . . . . . . . . 12
⊢
(!‘2) = 2 |
267 | 265, 266 | eqtrdi 2852 |
. . . . . . . . . . 11
⊢ (𝜑 →
(!‘(♯‘{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = 2) |
268 | 264, 267 | syl5eq 2848 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}}) = 2) |
269 | 262, 268 | eqtrd 2836 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}–1-1-onto→{((2^{nd} ‘(1^{st}
‘𝑇))‘((2^{nd} ‘𝑇) + 1)), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))}}) = 2) |
270 | 238, 269 | breqtrd 5059 |
. . . . . . . 8
⊢ (𝜑 →
(♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) ≤
2) |
271 | | breq1 5036 |
. . . . . . . 8
⊢
((♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) = 3 →
((♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) ≤ 2 ↔ 3 ≤
2)) |
272 | 270, 271 | syl5ibcom 248 |
. . . . . . 7
⊢ (𝜑 →
((♯‘{((2^{nd} ‘(1^{st} ‘𝑇)) ∘
{⟨(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)⟩, ⟨((2^{nd}
‘𝑇) + 1),
(2^{nd} ‘𝑇)⟩}), {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘(1^{st} ‘𝑇))‘(2^{nd} ‘𝑇))⟩, ⟨((2^{nd}
‘𝑇) + 1),
((2^{nd} ‘(1^{st} ‘𝑇))‘((2^{nd} ‘𝑇) + 1))⟩}, ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})}) = 3 → 3 ≤
2)) |
273 | 151, 272 | syld 47 |
. . . . . 6
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ≠ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) → 3 ≤
2)) |
274 | 273 | necon1bd 3008 |
. . . . 5
⊢ (𝜑 → (¬ 3 ≤ 2 →
((2^{nd} ‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}))) |
275 | 44, 274 | mpi 20 |
. . . 4
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩})) |
276 | | coires1 6088 |
. . . . 5
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)}))) =
((2^{nd} ‘(1^{st} ‘𝑇)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) |
277 | 128, 276 | eqtr4di 2854 |
. . . 4
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)})) = ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})))) |
278 | 275, 277 | uneq12d 4094 |
. . 3
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑈)) ↾ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}) ∪ ((2^{nd}
‘(1^{st} ‘𝑈)) ↾ ((1...𝑁) ∖ {(2^{nd} ‘𝑇), ((2^{nd} ‘𝑇) + 1)}))) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))) |
279 | 39, 278 | eqtr3d 2838 |
. 2
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑈)) = (((2^{nd}
‘(1^{st} ‘𝑇)) ∘ {⟨(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) + 1)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)}))))) |
280 | | coundi 6071 |
. 2
⊢
((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)⟩,
⟨((2^{nd} ‘𝑇) + 1), (2^{nd} ‘𝑇)⟩}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2^{nd}
‘𝑇), ((2^{nd}
‘𝑇) +
1)})))) |
281 | 279, 280 | eqtr4di 2854 |
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)}))))) |