Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem9 Structured version   Visualization version   GIF version

Theorem poimirlem9 37010
Description: Lemma for poimir 37034, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((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}))))}
poimirlem9.1 (𝜑𝑇𝑆)
poimirlem9.2 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
poimirlem9.3 (𝜑𝑈𝑆)
poimirlem9.4 (𝜑 → (2nd ‘(1st𝑈)) ≠ (2nd ‘(1st𝑇)))
Assertion
Ref Expression
poimirlem9 (𝜑 → (2nd ‘(1st𝑈)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
Distinct variable groups:   𝑓,𝑗,𝑡,𝑦   𝜑,𝑗,𝑦   𝑗,𝐹,𝑦   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝜑,𝑡   𝑓,𝐾,𝑗,𝑡   𝑓,𝑁,𝑡   𝑇,𝑓   𝑈,𝑓   𝑓,𝐹,𝑡   𝑡,𝑇   𝑡,𝑈   𝑆,𝑗,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem9
StepHypRef Expression
1 resundi 5989 . . . 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 (𝜑𝑁 ∈ ℕ)
32nncnd 12232 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
4 npcan1 11643 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53, 4syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
62nnzd 12589 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
7 peano2zm 12609 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8 uzid 12841 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9 peano2uz 12889 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
106, 7, 8, 94syl 19 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
115, 10eqeltrrd 2828 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
12 fzss2 13547 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
1513, 14sseldd 3978 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
16 fzp1elp1 13560 . . . . . . . . . 10 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
185oveq2d 7421 . . . . . . . . 9 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
1917, 18eleqtrd 2829 . . . . . . . 8 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
2015, 19prssd 4820 . . . . . . 7 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
21 undif 4476 . . . . . . 7 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
2220, 21sylib 217 . . . . . 6 (𝜑 → ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
2322reseq2d 5975 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) ↾ (1...𝑁)))
24 poimirlem9.3 . . . . . . . 8 (𝜑𝑈𝑆)
25 elrabi 3672 . . . . . . . . 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}))))}
2725, 26eleq2s 2845 . . . . . . . 8 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28 xp1st 8006 . . . . . . . 8 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29 xp2nd 8007 . . . . . . . 8 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
3024, 27, 28, 294syl 19 . . . . . . 7 (𝜑 → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
31 fvex 6898 . . . . . . . 8 (2nd ‘(1st𝑈)) ∈ V
32 f1oeq1 6815 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3331, 32elab 3663 . . . . . . 7 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
3430, 33sylib 217 . . . . . 6 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
35 f1ofn 6828 . . . . . 6 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)) Fn (1...𝑁))
36 fnresdm 6663 . . . . . 6 ((2nd ‘(1st𝑈)) Fn (1...𝑁) → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3734, 35, 363syl 18 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3823, 37eqtrd 2766 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
391, 38eqtr3id 2780 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
40 2lt3 12388 . . . . . 6 2 < 3
41 2re 12290 . . . . . . 7 2 ∈ ℝ
42 3re 12296 . . . . . . 7 3 ∈ ℝ
4341, 42ltnlei 11339 . . . . . 6 (2 < 3 ↔ ¬ 3 ≤ 2)
4440, 43mpbi 229 . . . . 5 ¬ 3 ≤ 2
45 df-pr 4626 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
4645coeq2i 5854 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
47 coundi 6240 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
4846, 47eqtri 2754 . . . . . . . . . 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 3672 . . . . . . . . . . . . . . . . . . . . 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...𝑁)))
5150, 26eleq2s 2845 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52 xp1st 8006 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53 xp2nd 8007 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5449, 51, 52, 534syl 19 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
55 fvex 6898 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
56 f1oeq1 6815 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
5755, 56elab 3663 . . . . . . . . . . . . . . . . . . 19 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
5854, 57sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
59 f1of1 6826 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁))
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁))
6119snssd 4807 . . . . . . . . . . . . . . . . 17 (𝜑 → {((2nd𝑇) + 1)} ⊆ (1...𝑁))
62 f1ores 6841 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ {((2nd𝑇) + 1)} ⊆ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
6360, 61, 62syl2anc 583 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
64 f1of 6827 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}) → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
66 f1ofn 6828 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
6758, 66syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
68 fnsnfv 6964 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
6967, 19, 68syl2anc 583 . . . . . . . . . . . . . . . 16 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
7069feq3d 6698 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} ↔ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)})))
7165, 70mpbird 257 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
72 eqid 2726 . . . . . . . . . . . . . . 15 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}
73 fvex 6898 . . . . . . . . . . . . . . . 16 (2nd𝑇) ∈ V
74 ovex 7438 . . . . . . . . . . . . . . . 16 ((2nd𝑇) + 1) ∈ V
7573, 74fsn 7129 . . . . . . . . . . . . . . 15 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}:{(2nd𝑇)}⟶{((2nd𝑇) + 1)} ↔ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩})
7672, 75mpbir 230 . . . . . . . . . . . . . 14 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}:{(2nd𝑇)}⟶{((2nd𝑇) + 1)}
77 fco2 6738 . . . . . . . . . . . . . 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))})
7871, 76, 77sylancl 585 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}):{(2nd𝑇)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
79 fvex 6898 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V
8079fconst2 7202 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}):{(2nd𝑇)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} ↔ ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}))
8178, 80sylib 217 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}))
8273, 79xpsn 7135 . . . . . . . . . . . 12 ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
8381, 82eqtrdi 2782 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
8483uneq1d 4157 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
8548, 84eqtrid 2778 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
86 elfznn 13536 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
8714, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) ∈ ℕ)
8887nnred 12231 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) ∈ ℝ)
8988ltp1d 12148 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
9088, 89ltned 11354 . . . . . . . . . . . . . 14 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
9190necomd 2990 . . . . . . . . . . . . 13 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
92 f1veqaeq 7252 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ (((2nd𝑇) + 1) ∈ (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁))) → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9360, 19, 15, 92syl12anc 834 . . . . . . . . . . . . . 14 (𝜑 → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9493necon3d 2955 . . . . . . . . . . . . 13 (𝜑 → (((2nd𝑇) + 1) ≠ (2nd𝑇) → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9591, 94mpd 15 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9695neneqd 2939 . . . . . . . . . . 11 (𝜑 → ¬ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9773, 79opth 5469 . . . . . . . . . . . 12 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩ ↔ ((2nd𝑇) = (2nd𝑇) ∧ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9897simprbi 496 . . . . . . . . . . 11 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩ → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9996, 98nsyl 140 . . . . . . . . . 10 (𝜑 → ¬ ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩)
10090neneqd 2939 . . . . . . . . . . 11 (𝜑 → ¬ (2nd𝑇) = ((2nd𝑇) + 1))
10173, 79opth1 5468 . . . . . . . . . . 11 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ → (2nd𝑇) = ((2nd𝑇) + 1))
102100, 101nsyl 140 . . . . . . . . . 10 (𝜑 → ¬ ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩)
103 opex 5457 . . . . . . . . . . . . . . 15 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ V
104103snid 4659 . . . . . . . . . . . . . 14 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
105 elun1 4171 . . . . . . . . . . . . . 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𝑇)⟩})))
106104, 105ax-mp 5 . . . . . . . . . . . . 13 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
107 eleq2 2816 . . . . . . . . . . . . 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))⟩}))
108106, 107mpbii 232 . . . . . . . . . . . 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))⟩})
109103elpr 4646 . . . . . . . . . . . . 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 986 . . . . . . . . . . . . 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))⟩))
111109, 110bitri 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))⟩))
112108, 111sylib 217 . . . . . . . . . . 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))⟩))
113112necon2ai 2964 . . . . . . . . . 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))⟩})
11499, 102, 113syl2anc 583 . . . . . . . . 9 (𝜑 → ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11585, 114eqnetrd 3002 . . . . . . . 8 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
116 fnressn 7152 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
11767, 15, 116syl2anc 583 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
118 fnressn 7152 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11967, 19, 118syl2anc 583 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
120117, 119uneq12d 4159 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}))
121 df-pr 4626 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
122121reseq2i 5972 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
123 resundi 5989 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
124122, 123eqtri 2754 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
125 df-pr 4626 . . . . . . . . . 10 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
126120, 124, 1253eqtr4g 2791 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
127 poimirlem9.4 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑈)) ≠ (2nd ‘(1st𝑇)))
1282, 26, 49, 14, 24poimirlem8 37009 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
129 uneq12 4153 . . . . . . . . . . . . . 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 5989 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
13122reseq2d 5975 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ (1...𝑁)))
132 fnresdm 6663 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) Fn (1...𝑁) → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
13358, 66, 1323syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
134131, 133eqtrd 2766 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
135130, 134eqtr3id 2780 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
13639, 135eqeq12d 2742 . . . . . . . . . . . . . 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𝑇))))
137129, 136imbitrid 243 . . . . . . . . . . . . 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𝑇))))
138128, 137mpan2d 691 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
139138necon3d 2955 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) ≠ (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)})))
140127, 139mpd 15 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
141140necomd 2990 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
142126, 141eqnetrrd 3003 . . . . . . . 8 (𝜑 → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
143 prex 5425 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
14455, 143coex 7920 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∈ V
145 prex 5425 . . . . . . . . . . 11 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∈ V
14631resex 6023 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V
147 hashtpg 14452 . . . . . . . . . . 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))
148144, 145, 146, 147mp3an 1457 . . . . . . . . . 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)
149148biimpi 215 . . . . . . . . 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)
1501493expia 1118 . . . . . . . 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))
151115, 142, 150syl2anc 583 . . . . . . 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 5425 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ V
153 prex 5425 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ V
154152, 153mapval 8834 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}
155 prfi 9324 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin
156 prfi 9324 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin
157 mapfi 9350 . . . . . . . . . . . . 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)
158155, 156, 157mp2an 689 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
159154, 158eqeltrri 2824 . . . . . . . . . . 11 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
160 f1of 6827 . . . . . . . . . . . 12 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
161160ss2abi 4058 . . . . . . . . . . 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 9175 . . . . . . . . . . 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)
163159, 161, 162mp2an 689 . . . . . . . . . 10 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
16419, 15prssd 4820 . . . . . . . . . . . . . . 15 (𝜑 → {((2nd𝑇) + 1), (2nd𝑇)} ⊆ (1...𝑁))
165 f1ores 6841 . . . . . . . . . . . . . . 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𝑇)}))
16660, 164, 165syl2anc 583 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}):{((2nd𝑇) + 1), (2nd𝑇)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}))
167 fnimapr 6969 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
16867, 19, 15, 167syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
169168f1oeq3d 6824 . . . . . . . . . . . . . 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𝑇))}))
170166, 169mpbid 231 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}):{((2nd𝑇) + 1), (2nd𝑇)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
171 f1oprg 6872 . . . . . . . . . . . . . . 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𝑇)}))
17273, 74, 74, 73, 171mp4an 690 . . . . . . . . . . . . . 14 (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≠ (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
17390, 91, 172syl2anc 583 . . . . . . . . . . . . 13 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
174 f1oco 6850 . . . . . . . . . . . . 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𝑇))})
175170, 173, 174syl2anc 583 . . . . . . . . . . . 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 6215 . . . . . . . . . . . . . . 15 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
17773, 74, 176mp2an 689 . . . . . . . . . . . . . 14 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)}
178177eqimssi 4037 . . . . . . . . . . . . 13 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ {((2nd𝑇) + 1), (2nd𝑇)}
179 cores 6242 . . . . . . . . . . . . 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 6815 . . . . . . . . . . . . 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𝑇))}))
181178, 179, 180mp2b 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𝑇))})
182175, 181sylib 217 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
18395necomd 2990 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
184 fvex 6898 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V
185 f1oprg 6872 . . . . . . . . . . . . . 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))}))
18673, 184, 74, 79, 185mp4an 690 . . . . . . . . . . . . 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))})
18790, 183, 186syl2anc 583 . . . . . . . . . . . 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 6817 . . . . . . . . . . . . 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𝑇))}))
190188, 189ax-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𝑇))})
191187, 190sylib 217 . . . . . . . . . . 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 6826 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–1-1→(1...𝑁))
19334, 192syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1→(1...𝑁))
194 f1ores 6841 . . . . . . . . . . . . 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)}))
195193, 20, 194syl2anc 583 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
196 dff1o3 6833 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
197196simprbi 496 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
198 imadif 6626 . . . . . . . . . . . . . . . 16 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
19934, 197, 1983syl 18 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
200 f1ofo 6834 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
201 foima 6804 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
20234, 200, 2013syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
203 f1ofo 6834 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
204 foima 6804 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
20558, 203, 2043syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
206202, 205eqtr4d 2769 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ (1...𝑁)))
207128rneqd 5931 . . . . . . . . . . . . . . . . 17 (𝜑 → ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
208 df-ima 5682 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
209 df-ima 5682 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
210207, 208, 2093eqtr4g 2791 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
211206, 210difeq12d 4118 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
212 dff1o3 6833 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
213212simprbi 496 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
214 imadif 6626 . . . . . . . . . . . . . . . . 17 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
21558, 213, 2143syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
216 dfin4 4262 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
217 sseqin2 4210 . . . . . . . . . . . . . . . . . . 19 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
21820, 217sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
219216, 218eqtr3id 2780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = {(2nd𝑇), ((2nd𝑇) + 1)})
220219imaeq2d 6053 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
221215, 220eqtr3d 2768 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
222199, 211, 2213eqtrd 2770 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
223219imaeq2d 6053 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
224 fnimapr 6969 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
22567, 15, 19, 224syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
226225, 188eqtrdi 2782 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
227222, 223, 2263eqtr3d 2774 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
228227f1oeq3d 6824 . . . . . . . . . . . 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𝑇))}))
229195, 228mpbid 231 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
230 ssabral 4054 . . . . . . . . . . . 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 6815 . . . . . . . . . . . . 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 6815 . . . . . . . . . . . . 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 6815 . . . . . . . . . . . . 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𝑇))}))
234144, 145, 146, 231, 232, 233raltp 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𝑇))}))
235230, 234bitri 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𝑇))}))
236182, 191, 229, 235syl3anbrc 1340 . . . . . . . . . 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 14374 . . . . . . . . . 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𝑇))}}))
238163, 236, 237sylancr 586 . . . . . . . . 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𝑇))}}))
239153enref 8983 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}
240 hashprg 14360 . . . . . . . . . . . . . . . 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))
24179, 184, 240mp2an 689 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ↔ (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
24295, 241sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
243 hashprg 14360 . . . . . . . . . . . . . . . 16 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2))
24473, 74, 243mp2an 689 . . . . . . . . . . . . . . 15 ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
24590, 244sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
246242, 245eqtr4d 2769 . . . . . . . . . . . . 13 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
247 hashen 14312 . . . . . . . . . . . . . 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)}))
248155, 156, 247mp2an 689 . . . . . . . . . . . . 13 ((♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) ↔ {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
249246, 248sylib 217 . . . . . . . . . . . 12 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
250 hashfacen 14419 . . . . . . . . . . . 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)}})
251239, 249, 250sylancr 586 . . . . . . . . . . 11 (𝜑 → {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ≈ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}})
252153, 153mapval 8834 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
253 mapfi 9350 . . . . . . . . . . . . . . 15 (({(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin)
254156, 156, 253mp2an 689 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
255252, 254eqeltrri 2824 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
256 f1of 6827 . . . . . . . . . . . . . 14 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)})
257256ss2abi 4058 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
258 ssfi 9175 . . . . . . . . . . . . 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)
259255, 257, 258mp2an 689 . . . . . . . . . . . 12 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
260 hashen 14312 . . . . . . . . . . . 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)}}))
261163, 259, 260mp2an 689 . . . . . . . . . . 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)}})
262251, 261sylibr 233 . . . . . . . . . 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 14425 . . . . . . . . . . . 12 ({(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})))
264156, 263ax-mp 5 . . . . . . . . . . 11 (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
265245fveq2d 6889 . . . . . . . . . . . 12 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = (!‘2))
266 fac2 14244 . . . . . . . . . . . 12 (!‘2) = 2
267265, 266eqtrdi 2782 . . . . . . . . . . 11 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = 2)
268264, 267eqtrid 2778 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = 2)
269262, 268eqtrd 2766 . . . . . . . . 9 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = 2)
270238, 269breqtrd 5167 . . . . . . . 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 5144 . . . . . . . 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))
272270, 271syl5ibcom 244 . . . . . . 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))
273151, 272syld 47 . . . . . 6 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) → 3 ≤ 2))
274273necon1bd 2952 . . . . 5 (𝜑 → (¬ 3 ≤ 2 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
27544, 274mpi 20 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
276 coires1 6257 . . . . 5 ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
277128, 276eqtr4di 2784 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
278275, 277uneq12d 4159 . . 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)})))))
27939, 278eqtr3d 2768 . 2 (𝜑 → (2nd ‘(1st𝑈)) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
280 coundi 6240 . 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)}))))
281279, 280eqtr4di 2784 1 (𝜑 → (2nd ‘(1st𝑈)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3a 1084   = wceq 1533  wcel 2098  {cab 2703  wne 2934  wral 3055  {crab 3426  Vcvv 3468  csb 3888  cdif 3940  cun 3941  cin 3942  wss 3943  ifcif 4523  {csn 4623  {cpr 4625  {ctp 4627  cop 4629   class class class wbr 5141  cmpt 5224   I cid 5566   × cxp 5667  ccnv 5668  ran crn 5670  cres 5671  cima 5672  ccom 5673  Fun wfun 6531   Fn wfn 6532  wf 6533  1-1wf1 6534  ontowfo 6535  1-1-ontowf1o 6536  cfv 6537  (class class class)co 7405  f cof 7665  1st c1st 7972  2nd c2nd 7973  m cmap 8822  cen 8938  Fincfn 8941  cc 11110  0cc0 11112  1c1 11113   + caddc 11115   < clt 11252  cle 11253  cmin 11448  cn 12216  2c2 12271  3c3 12272  cz 12562  cuz 12826  ...cfz 13490  ..^cfzo 13633  !cfa 14238  chash 14295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-oadd 8471  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13491  df-fzo 13634  df-seq 13973  df-fac 14239  df-bc 14268  df-hash 14296
This theorem is referenced by:  poimirlem22  37023
  Copyright terms: Public domain W3C validator