Proof of Theorem poimirlem9
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | resundi 6010 | . . . 4
⊢
((2nd ‘(1st ‘𝑈)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
(((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 2 |  | poimir.0 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 | 2 | nncnd 12283 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 4 |  | npcan1 11689 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) | 
| 5 | 3, 4 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) | 
| 6 | 2 | nnzd 12642 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 7 |  | peano2zm 12662 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) | 
| 8 |  | uzid 12894 | . . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 9 |  | peano2uz 12944 | . . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 10 | 6, 7, 8, 9 | 4syl 19 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 11 | 5, 10 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) | 
| 12 |  | fzss2 13605 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) | 
| 14 |  | poimirlem9.2 | . . . . . . . . 9
⊢ (𝜑 → (2nd
‘𝑇) ∈
(1...(𝑁 −
1))) | 
| 15 | 13, 14 | sseldd 3983 | . . . . . . . 8
⊢ (𝜑 → (2nd
‘𝑇) ∈ (1...𝑁)) | 
| 16 |  | fzp1elp1 13618 | . . . . . . . . . 10
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) | 
| 17 | 14, 16 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) | 
| 18 | 5 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) | 
| 19 | 17, 18 | eleqtrd 2842 | . . . . . . . 8
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
(1...𝑁)) | 
| 20 | 15, 19 | prssd 4821 | . . . . . . 7
⊢ (𝜑 → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
(1...𝑁)) | 
| 21 |  | undif 4481 | . . . . . . 7
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) =
(1...𝑁)) | 
| 22 | 20, 21 | sylib 218 | . . . . . 6
⊢ (𝜑 → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) = (1...𝑁)) | 
| 23 | 22 | reseq2d 5996 | . . . . 5
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
((2nd ‘(1st ‘𝑈)) ↾ (1...𝑁))) | 
| 24 |  | poimirlem9.3 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) | 
| 25 |  | elrabi 3686 | . . . . . . . . 9
⊢ (𝑈 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 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(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} | 
| 27 | 25, 26 | eleq2s 2858 | . . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) | 
| 28 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 29 |  | xp2nd 8048 | . . . . . . . 8
⊢
((1st ‘𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 30 | 24, 27, 28, 29 | 4syl 19 | . . . . . . 7
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 31 |  | fvex 6918 | . . . . . . . 8
⊢
(2nd ‘(1st ‘𝑈)) ∈ V | 
| 32 |  | f1oeq1 6835 | . . . . . . . 8
⊢ (𝑓 = (2nd
‘(1st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))) | 
| 33 | 31, 32 | elab 3678 | . . . . . . 7
⊢
((2nd ‘(1st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 34 | 30, 33 | sylib 218 | . . . . . 6
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 35 |  | f1ofn 6848 | . . . . . 6
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑈)) Fn (1...𝑁)) | 
| 36 |  | fnresdm 6686 | . . . . . 6
⊢
((2nd ‘(1st ‘𝑈)) Fn (1...𝑁) → ((2nd
‘(1st ‘𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st
‘𝑈))) | 
| 37 | 34, 35, 36 | 3syl 18 | . . . . 5
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st
‘𝑈))) | 
| 38 | 23, 37 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
(2nd ‘(1st ‘𝑈))) | 
| 39 | 1, 38 | eqtr3id 2790 | . . 3
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (2nd
‘(1st ‘𝑈))) | 
| 40 |  | 2lt3 12439 | . . . . . 6
⊢ 2 <
3 | 
| 41 |  | 2re 12341 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 42 |  | 3re 12347 | . . . . . . 7
⊢ 3 ∈
ℝ | 
| 43 | 41, 42 | ltnlei 11383 | . . . . . 6
⊢ (2 < 3
↔ ¬ 3 ≤ 2) | 
| 44 | 40, 43 | mpbi 230 | . . . . 5
⊢  ¬ 3
≤ 2 | 
| 45 |  | df-pr 4628 | . . . . . . . . . . . 12
⊢
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉} ∪
{〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) | 
| 46 | 45 | coeq2i 5870 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) = ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉} ∪
{〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) | 
| 47 |  | coundi 6266 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉} ∪
{〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) = (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉})
∪ ((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) | 
| 48 | 46, 47 | eqtri 2764 | . . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) = (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉})
∪ ((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) | 
| 49 |  | poimirlem9.1 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ 𝑆) | 
| 50 |  | elrabi 3686 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) | 
| 51 | 50, 26 | eleq2s 2858 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) | 
| 52 |  | xp1st 8047 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 53 |  | xp2nd 8048 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 54 | 49, 51, 52, 53 | 4syl 19 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 55 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V | 
| 56 |  | f1oeq1 6835 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) | 
| 57 | 55, 56 | elab 3678 | . . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 58 | 54, 57 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 59 |  | f1of1 6846 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) | 
| 61 | 19 | snssd 4808 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {((2nd
‘𝑇) + 1)} ⊆
(1...𝑁)) | 
| 62 |  | f1ores 6861 | . . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2nd ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1)})) | 
| 63 | 60, 61, 62 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1)})) | 
| 64 |  | f1of 6847 | . . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1)}) → ((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶((2nd ‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1)})) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶((2nd ‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1)})) | 
| 66 |  | f1ofn 6848 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) | 
| 67 | 58, 66 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) | 
| 68 |  | fnsnfv 6987 | . . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} = ((2nd
‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1)})) | 
| 69 | 67, 19, 68 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} = ((2nd
‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1)})) | 
| 70 | 69 | feq3d 6722 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} ↔ ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶((2nd ‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1)}))) | 
| 71 | 65, 70 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 72 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉} = {〈(2nd
‘𝑇), ((2nd
‘𝑇) +
1)〉} | 
| 73 |  | fvex 6918 | . . . . . . . . . . . . . . . 16
⊢
(2nd ‘𝑇) ∈ V | 
| 74 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑇) + 1) ∈ V | 
| 75 | 73, 74 | fsn 7154 | . . . . . . . . . . . . . . 15
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉}:{(2nd ‘𝑇)}⟶{((2nd
‘𝑇) + 1)} ↔
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉} = {〈(2nd
‘𝑇), ((2nd
‘𝑇) +
1)〉}) | 
| 76 | 72, 75 | mpbir 231 | . . . . . . . . . . . . . 14
⊢
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉}:{(2nd ‘𝑇)}⟶{((2nd
‘𝑇) +
1)} | 
| 77 |  | fco2 6761 | . . . . . . . . . . . . . 14
⊢
((((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}):{((2nd
‘𝑇) +
1)}⟶{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} ∧
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉}:{(2nd ‘𝑇)}⟶{((2nd
‘𝑇) + 1)}) →
((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) +
1)〉}):{(2nd ‘𝑇)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 78 | 71, 76, 77 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) +
1)〉}):{(2nd ‘𝑇)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 79 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ∈
V | 
| 80 | 79 | fconst2 7226 | . . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) +
1)〉}):{(2nd ‘𝑇)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} ↔ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉}) =
({(2nd ‘𝑇)} × {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))})) | 
| 81 | 78, 80 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉}) =
({(2nd ‘𝑇)} × {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))})) | 
| 82 | 73, 79 | xpsn 7160 | . . . . . . . . . . . 12
⊢
({(2nd ‘𝑇)} × {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) =
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} | 
| 83 | 81, 82 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉}) =
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 84 | 83 | uneq1d 4166 | . . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉})
∪ ((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) = ({〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}))) | 
| 85 | 48, 84 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) =
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}))) | 
| 86 |  | elfznn 13594 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℕ) | 
| 87 | 14, 86 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℕ) | 
| 88 | 87 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) | 
| 89 | 88 | ltp1d 12199 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) | 
| 90 | 88, 89 | ltned 11398 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2nd
‘𝑇) ≠
((2nd ‘𝑇)
+ 1)) | 
| 91 | 90 | necomd 2995 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≠
(2nd ‘𝑇)) | 
| 92 |  | f1veqaeq 7278 | . . . . . . . . . . . . . . 15
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ (((2nd ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2nd
‘𝑇) ∈ (1...𝑁))) → (((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) = ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) → ((2nd
‘𝑇) + 1) =
(2nd ‘𝑇))) | 
| 93 | 60, 19, 15, 92 | syl12anc 836 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) = ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) → ((2nd
‘𝑇) + 1) =
(2nd ‘𝑇))) | 
| 94 | 93 | necon3d 2960 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ≠
(2nd ‘𝑇)
→ ((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ≠ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)))) | 
| 95 | 91, 94 | mpd 15 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ≠ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))) | 
| 96 | 95 | neneqd 2944 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) = ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))) | 
| 97 | 73, 79 | opth 5480 | . . . . . . . . . . . 12
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ↔ ((2nd
‘𝑇) = (2nd
‘𝑇) ∧
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) = ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)))) | 
| 98 | 97 | simprbi 496 | . . . . . . . . . . 11
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 → ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) = ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))) | 
| 99 | 96, 98 | nsyl 140 | . . . . . . . . . 10
⊢ (𝜑 → ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉) | 
| 100 | 90 | neneqd 2944 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (2nd
‘𝑇) =
((2nd ‘𝑇)
+ 1)) | 
| 101 | 73, 79 | opth1 5479 | . . . . . . . . . . 11
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉 →
(2nd ‘𝑇) =
((2nd ‘𝑇)
+ 1)) | 
| 102 | 100, 101 | nsyl 140 | . . . . . . . . . 10
⊢ (𝜑 → ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉) | 
| 103 |  | opex 5468 | . . . . . . . . . . . . . . 15
⊢
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
V | 
| 104 | 103 | snid 4661 | . . . . . . . . . . . . . 14
⊢
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} | 
| 105 |  | elun1 4181 | . . . . . . . . . . . . . 14
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} →
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}))) | 
| 106 | 104, 105 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) | 
| 107 |  | eleq2 2829 | . . . . . . . . . . . . 13
⊢
(({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} →
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) ↔ 〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) +
1))〉})) | 
| 108 | 106, 107 | mpbii 233 | . . . . . . . . . . . 12
⊢
(({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} →
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 109 | 103 | elpr 4649 | . . . . . . . . . . . . 13
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ↔
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∨
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉)) | 
| 110 |  | oran 991 | . . . . . . . . . . . . 13
⊢
((〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∨
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉) ↔ ¬
(¬ 〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∧ ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉)) | 
| 111 | 109, 110 | bitri 275 | . . . . . . . . . . . 12
⊢
(〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 ∈
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ↔ ¬
(¬ 〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∧ ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉)) | 
| 112 | 108, 111 | sylib 218 | . . . . . . . . . . 11
⊢
(({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} → ¬
(¬ 〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∧ ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉)) | 
| 113 | 112 | necon2ai 2969 | . . . . . . . . . 10
⊢ ((¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉 ∧ ¬
〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉 =
〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉) →
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) ≠ {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 114 | 99, 102, 113 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ({〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∪
((2nd ‘(1st ‘𝑇)) ∘ {〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉})) ≠ {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 115 | 85, 114 | eqnetrd 3007 | . . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ≠
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 116 |  | fnressn 7177 | . . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (2nd ‘𝑇) ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇)}) = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉}) | 
| 117 | 67, 15, 116 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇)}) = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉}) | 
| 118 |  | fnressn 7177 | . . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}) =
{〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 119 | 67, 19, 118 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)}) =
{〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 120 | 117, 119 | uneq12d 4168 | . . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)})) =
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉} ∪
{〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) +
1))〉})) | 
| 121 |  | df-pr 4628 | . . . . . . . . . . . 12
⊢
{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} = ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) +
1)}) | 
| 122 | 121 | reseq2i 5993 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ↾ ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) +
1)})) | 
| 123 |  | resundi 6010 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ↾ ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) + 1)})) =
(((2nd ‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)})) | 
| 124 | 122, 123 | eqtri 2764 | . . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = (((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1)})) | 
| 125 |  | df-pr 4628 | . . . . . . . . . 10
⊢
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} =
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉} ∪
{〈((2nd ‘𝑇) + 1), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 126 | 120, 124,
125 | 3eqtr4g 2801 | . . . . . . . . 9
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) =
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}) | 
| 127 |  | poimirlem9.4 | . . . . . . . . . . 11
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)) ≠ (2nd
‘(1st ‘𝑇))) | 
| 128 | 2, 26, 49, 14, 24 | poimirlem8 37636 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 129 |  | uneq12 4162 | . . . . . . . . . . . . . 14
⊢
((((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∧ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) →
(((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 130 |  | resundi 6010 | . . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
(((2nd ‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 131 | 22 | reseq2d 5996 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
((2nd ‘(1st ‘𝑇)) ↾ (1...𝑁))) | 
| 132 |  | fnresdm 6686 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) → ((2nd
‘(1st ‘𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st
‘𝑇))) | 
| 133 | 58, 66, 132 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st
‘𝑇))) | 
| 134 | 131, 133 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
(2nd ‘(1st ‘𝑇))) | 
| 135 | 130, 134 | eqtr3id 2790 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (2nd
‘(1st ‘𝑇))) | 
| 136 | 39, 135 | eqeq12d 2752 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) ↔
(2nd ‘(1st ‘𝑈)) = (2nd ‘(1st
‘𝑇)))) | 
| 137 | 129, 136 | imbitrid 244 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∧ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) →
(2nd ‘(1st ‘𝑈)) = (2nd ‘(1st
‘𝑇)))) | 
| 138 | 128, 137 | mpan2d 694 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) → (2nd
‘(1st ‘𝑈)) = (2nd ‘(1st
‘𝑇)))) | 
| 139 | 138 | necon3d 2960 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ≠ (2nd
‘(1st ‘𝑇)) → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 140 | 127, 139 | mpd 15 | . . . . . . . . . 10
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 141 | 140 | necomd 2995 | . . . . . . . . 9
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 142 | 126, 141 | eqnetrrd 3008 | . . . . . . . 8
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ≠
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 143 |  | prex 5436 | . . . . . . . . . . . 12
⊢
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∈ V | 
| 144 | 55, 143 | coex 7953 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ∈
V | 
| 145 |  | prex 5436 | . . . . . . . . . . 11
⊢
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∈
V | 
| 146 | 31 | resex 6046 | . . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∈
V | 
| 147 |  | hashtpg 14525 | . . . . . . . . . . 11
⊢
((((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ∈ V ∧
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∈ V ∧
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∈ V) →
((((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ≠
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∧
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ≠
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∧ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) ↔
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) =
3)) | 
| 148 | 144, 145,
146, 147 | mp3an 1462 | . . . . . . . . . 10
⊢
((((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ≠
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∧
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ≠
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∧ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) ↔
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) = 3) | 
| 149 | 148 | biimpi 216 | . . . . . . . . 9
⊢
((((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ≠
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∧
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ≠
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∧ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) = 3) | 
| 150 | 149 | 3expia 1121 | . . . . . . . 8
⊢
((((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ≠
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ∧
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} ≠
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) →
(((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) =
3)) | 
| 151 | 115, 142,
150 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) =
3)) | 
| 152 |  | prex 5436 | . . . . . . . . . . . . 13
⊢
{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∈ V | 
| 153 |  | prex 5436 | . . . . . . . . . . . . 13
⊢
{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∈ V | 
| 154 | 152, 153 | mapval 8879 | . . . . . . . . . . . 12
⊢
({((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↑m
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) = {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} | 
| 155 |  | prfi 9364 | . . . . . . . . . . . . 13
⊢
{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∈ Fin | 
| 156 |  | prfi 9364 | . . . . . . . . . . . . 13
⊢
{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∈ Fin | 
| 157 |  | mapfi 9389 | . . . . . . . . . . . . 13
⊢
(({((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∈ Fin ∧
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)} ∈ Fin) → ({((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↑m
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∈ Fin) | 
| 158 | 155, 156,
157 | mp2an 692 | . . . . . . . . . . . 12
⊢
({((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↑m
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∈ Fin | 
| 159 | 154, 158 | eqeltrri 2837 | . . . . . . . . . . 11
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈ Fin | 
| 160 |  | f1of 6847 | . . . . . . . . . . . 12
⊢ (𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} → 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 161 | 160 | ss2abi 4066 | . . . . . . . . . . 11
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} | 
| 162 |  | ssfi 9214 | . . . . . . . . . . 11
⊢ (({𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) → {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈
Fin) | 
| 163 | 159, 161,
162 | mp2an 692 | . . . . . . . . . 10
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈ Fin | 
| 164 | 19, 15 | prssd 4821 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → {((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}
⊆ (1...𝑁)) | 
| 165 |  | f1ores 6861 | . . . . . . . . . . . . . . 15
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)} ⊆
(1...𝑁)) →
((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1), (2nd ‘𝑇)})) | 
| 166 | 60, 164, 165 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1), (2nd ‘𝑇)})) | 
| 167 |  | fnimapr 6991 | . . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁) ∧ (2nd
‘𝑇) ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) =
{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 168 | 67, 19, 15, 167 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) =
{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 169 | 168 | f1oeq3d 6844 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→((2nd ‘(1st
‘𝑇)) “
{((2nd ‘𝑇)
+ 1), (2nd ‘𝑇)}) ↔ ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 170 | 166, 169 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 171 |  | f1oprg 6892 | . . . . . . . . . . . . . . 15
⊢
((((2nd ‘𝑇) ∈ V ∧ ((2nd
‘𝑇) + 1) ∈ V)
∧ (((2nd ‘𝑇) + 1) ∈ V ∧ (2nd
‘𝑇) ∈ V)) →
(((2nd ‘𝑇)
≠ ((2nd ‘𝑇) + 1) ∧ ((2nd ‘𝑇) + 1) ≠ (2nd
‘𝑇)) →
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)})) | 
| 172 | 73, 74, 74, 73, 171 | mp4an 693 | . . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘𝑇) + 1) ≠
(2nd ‘𝑇))
→ {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)}) | 
| 173 | 90, 91, 172 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)}) | 
| 174 |  | f1oco 6870 | . . . . . . . . . . . . 13
⊢
((((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}):{((2nd ‘𝑇) + 1), (2nd
‘𝑇)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∧ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)}) → (((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}):{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 175 | 170, 173,
174 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}):{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 176 |  | rnpropg 6241 | . . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑇) ∈ V ∧ ((2nd
‘𝑇) + 1) ∈ V)
→ ran {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) | 
| 177 | 73, 74, 176 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = {((2nd ‘𝑇) + 1), (2nd
‘𝑇)} | 
| 178 | 177 | eqimssi 4043 | . . . . . . . . . . . . 13
⊢ ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ⊆ {((2nd
‘𝑇) + 1),
(2nd ‘𝑇)} | 
| 179 |  | cores 6268 | . . . . . . . . . . . . 13
⊢ (ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ⊆ {((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}
→ (((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) = ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) | 
| 180 |  | f1oeq1 6835 | . . . . . . . . . . . . 13
⊢
((((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) = ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) →
((((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}):{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 181 | 178, 179,
180 | mp2b 10 | . . . . . . . . . . . 12
⊢
((((2nd ‘(1st ‘𝑇)) ↾ {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}):{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 182 | 175, 181 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 183 | 95 | necomd 2995 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))) | 
| 184 |  | fvex 6918 | . . . . . . . . . . . . . 14
⊢
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) ∈ V | 
| 185 |  | f1oprg 6892 | . . . . . . . . . . . . . 14
⊢
((((2nd ‘𝑇) ∈ V ∧ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ∈ V) ∧
(((2nd ‘𝑇)
+ 1) ∈ V ∧ ((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)) ∈ V))
→ (((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))) →
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))})) | 
| 186 | 73, 184, 74, 79, 185 | mp4an 693 | . . . . . . . . . . . . 13
⊢
(((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))) →
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 187 | 90, 183, 186 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 188 |  | prcom 4731 | . . . . . . . . . . . . 13
⊢
{((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} = {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} | 
| 189 |  | f1oeq3 6837 | . . . . . . . . . . . . 13
⊢
({((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} = {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} →
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} ↔
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 190 | 188, 189 | ax-mp 5 | . . . . . . . . . . . 12
⊢
({〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))} ↔
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 191 | 187, 190 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 192 |  | f1of1 6846 | . . . . . . . . . . . . . 14
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁)) | 
| 193 | 34, 192 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁)) | 
| 194 |  | f1ores 6861 | . . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1→(1...𝑁) ∧ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...𝑁)) → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑈)) “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) | 
| 195 | 193, 20, 194 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑈)) “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) | 
| 196 |  | dff1o3 6853 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑈)))) | 
| 197 | 196 | simprbi 496 | . . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑈))) | 
| 198 |  | imadif 6649 | . . . . . . . . . . . . . . . 16
⊢ (Fun
◡(2nd ‘(1st
‘𝑈)) →
((2nd ‘(1st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 199 | 34, 197, 198 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 200 |  | f1ofo 6854 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑈)):(1...𝑁)–onto→(1...𝑁)) | 
| 201 |  | foima 6824 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) = (1...𝑁)) | 
| 202 | 34, 200, 201 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) = (1...𝑁)) | 
| 203 |  | f1ofo 6854 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) | 
| 204 |  | foima 6824 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) | 
| 205 | 58, 203, 204 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) | 
| 206 | 202, 205 | eqtr4d 2779 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑁))) | 
| 207 | 128 | rneqd 5948 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ran ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 208 |  | df-ima 5697 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑈)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ran ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 209 |  | df-ima 5697 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ran ((2nd
‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 210 | 207, 208,
209 | 3eqtr4g 2801 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 211 | 206, 210 | difeq12d 4126 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 212 |  | dff1o3 6853 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) | 
| 213 | 212 | simprbi 496 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) | 
| 214 |  | imadif 6649 | . . . . . . . . . . . . . . . . 17
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 215 | 58, 213, 214 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})))) | 
| 216 |  | dfin4 4277 | . . . . . . . . . . . . . . . . . 18
⊢
((1...𝑁) ∩
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) = ((1...𝑁) ∖
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) | 
| 217 |  | sseqin2 4222 | . . . . . . . . . . . . . . . . . . 19
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) | 
| 218 | 20, 217 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) | 
| 219 | 216, 218 | eqtr3id 2790 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) | 
| 220 | 219 | imaeq2d 6077 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 221 | 215, 220 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 222 | 199, 211,
221 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 223 | 219 | imaeq2d 6077 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = ((2nd
‘(1st ‘𝑈)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 224 |  | fnimapr 6991 | . . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (2nd ‘𝑇) ∈ (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 225 | 67, 15, 19, 224 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)), ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))}) | 
| 226 | 225, 188 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 227 | 222, 223,
226 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 228 | 227 | f1oeq3d 6844 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→((2nd ‘(1st
‘𝑈)) “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ↔ ((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 229 | 195, 228 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 230 |  | ssabral 4064 | . . . . . . . . . . . 12
⊢
({((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ↔ ∀𝑓 ∈ {((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) | 
| 231 |  | f1oeq1 6835 | . . . . . . . . . . . . 13
⊢ (𝑓 = ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) → (𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 232 |  | f1oeq1 6835 | . . . . . . . . . . . . 13
⊢ (𝑓 = {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉} → (𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 233 |  | f1oeq1 6835 | . . . . . . . . . . . . 13
⊢ (𝑓 = ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) → (𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 234 | 144, 145,
146, 231, 232, 233 | raltp 4704 | . . . . . . . . . . . 12
⊢
(∀𝑓 ∈
{((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ↔ (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∧ {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∧ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 235 | 230, 234 | bitri 275 | . . . . . . . . . . 11
⊢
({((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ↔ (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∧ {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∧ ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}):{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))})) | 
| 236 | 182, 191,
229, 235 | syl3anbrc 1343 | . . . . . . . . . 10
⊢ (𝜑 → {((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) | 
| 237 |  | hashss 14449 | . . . . . . . . . 10
⊢ (({𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈ Fin ∧
{((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}),
{〈(2nd ‘𝑇), ((2nd ‘(1st
‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) ≤
(♯‘{𝑓 ∣
𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}})) | 
| 238 | 163, 236,
237 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) ≤
(♯‘{𝑓 ∣
𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}})) | 
| 239 | 153 | enref 9026 | . . . . . . . . . . . 12
⊢
{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)} | 
| 240 |  | hashprg 14435 | . . . . . . . . . . . . . . . 16
⊢
((((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ∈ V ∧
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) ∈ V) →
(((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ≠ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ↔
(♯‘{((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))}) = 2)) | 
| 241 | 79, 184, 240 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢
(((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) ≠ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) ↔
(♯‘{((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))}) = 2) | 
| 242 | 95, 241 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘{((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))}) = 2) | 
| 243 |  | hashprg 14435 | . . . . . . . . . . . . . . . 16
⊢
(((2nd ‘𝑇) ∈ V ∧ ((2nd
‘𝑇) + 1) ∈ V)
→ ((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ↔
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = 2)) | 
| 244 | 73, 74, 243 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ↔
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = 2) | 
| 245 | 90, 244 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = 2) | 
| 246 | 242, 245 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝜑 →
(♯‘{((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))}) =
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 247 |  | hashen 14387 | . . . . . . . . . . . . . 14
⊢
(({((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ∈ Fin ∧
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)} ∈ Fin) → ((♯‘{((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}) =
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ↔ {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) | 
| 248 | 155, 156,
247 | mp2an 692 | . . . . . . . . . . . . 13
⊢
((♯‘{((2nd ‘(1st ‘𝑇))‘((2nd
‘𝑇) + 1)),
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇))}) =
(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ↔ {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) | 
| 249 | 246, 248 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝜑 → {((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) | 
| 250 |  | hashfacen 14494 | . . . . . . . . . . . 12
⊢
(({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∧
{((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))} ≈ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) →
{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) | 
| 251 | 239, 249,
250 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) | 
| 252 | 153, 153 | mapval 8879 | . . . . . . . . . . . . . 14
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ↑m {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) = {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} | 
| 253 |  | mapfi 9389 | . . . . . . . . . . . . . . 15
⊢
(({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∈ Fin ∧ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∈ Fin)
→ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ↑m {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ∈
Fin) | 
| 254 | 156, 156,
253 | mp2an 692 | . . . . . . . . . . . . . 14
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ↑m {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ∈
Fin | 
| 255 | 252, 254 | eqeltrri 2837 | . . . . . . . . . . . . 13
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ∈
Fin | 
| 256 |  | f1of 6847 | . . . . . . . . . . . . . 14
⊢ (𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} → 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) | 
| 257 | 256 | ss2abi 4066 | . . . . . . . . . . . . 13
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} | 
| 258 |  | ssfi 9214 | . . . . . . . . . . . . 13
⊢ (({𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ⊆ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) → {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ∈ Fin) | 
| 259 | 255, 257,
258 | mp2an 692 | . . . . . . . . . . . 12
⊢ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ∈ Fin | 
| 260 |  | hashen 14387 | . . . . . . . . . . . 12
⊢ (({𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ∈ Fin ∧ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}} ∈ Fin) →
((♯‘{𝑓 ∣
𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}})) | 
| 261 | 163, 259,
260 | mp2an 692 | . . . . . . . . . . 11
⊢
((♯‘{𝑓
∣ 𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) ↔ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}} ≈ {𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) | 
| 262 | 251, 261 | sylibr 234 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) = (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}})) | 
| 263 |  | hashfac 14498 | . . . . . . . . . . . 12
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∈ Fin →
(♯‘{𝑓 ∣
𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) =
(!‘(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | 
| 264 | 156, 263 | ax-mp 5 | . . . . . . . . . . 11
⊢
(♯‘{𝑓
∣ 𝑓:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) =
(!‘(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 265 | 245 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 →
(!‘(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = (!‘2)) | 
| 266 |  | fac2 14319 | . . . . . . . . . . . 12
⊢
(!‘2) = 2 | 
| 267 | 265, 266 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝜑 →
(!‘(♯‘{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = 2) | 
| 268 | 264, 267 | eqtrid 2788 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}}) = 2) | 
| 269 | 262, 268 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1)), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))}}) = 2) | 
| 270 | 238, 269 | breqtrd 5168 | . . . . . . . 8
⊢ (𝜑 →
(♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) ≤
2) | 
| 271 |  | breq1 5145 | . . . . . . . 8
⊢
((♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) = 3 →
((♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) ≤ 2 ↔ 3 ≤
2)) | 
| 272 | 270, 271 | syl5ibcom 245 | . . . . . . 7
⊢ (𝜑 →
((♯‘{((2nd ‘(1st ‘𝑇)) ∘
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}), {〈(2nd
‘𝑇), ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇))〉, 〈((2nd
‘𝑇) + 1),
((2nd ‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))〉}, ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})}) = 3 → 3 ≤
2)) | 
| 273 | 151, 272 | syld 47 | . . . . . 6
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ≠ ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) → 3 ≤
2)) | 
| 274 | 273 | necon1bd 2957 | . . . . 5
⊢ (𝜑 → (¬ 3 ≤ 2 →
((2nd ‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}))) | 
| 275 | 44, 274 | mpi 20 | . . . 4
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉})) | 
| 276 |  | coires1 6283 | . . . . 5
⊢
((2nd ‘(1st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) =
((2nd ‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) | 
| 277 | 128, 276 | eqtr4di 2794 | . . . 4
⊢ (𝜑 → ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd
‘(1st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})))) | 
| 278 | 275, 277 | uneq12d 4168 | . . 3
⊢ (𝜑 → (((2nd
‘(1st ‘𝑈)) ↾ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ((2nd
‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ∪ ((2nd
‘(1st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))) | 
| 279 | 39, 278 | eqtr3d 2778 | . 2
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)) = (((2nd
‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ∪ ((2nd
‘(1st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))) | 
| 280 |  | coundi 6266 | . 2
⊢
((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) = (((2nd ‘(1st ‘𝑇)) ∘ {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) ∪ ((2nd
‘(1st ‘𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})))) | 
| 281 | 279, 280 | eqtr4di 2794 | 1
⊢ (𝜑 → (2nd
‘(1st ‘𝑈)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))) |