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 37158
Description: Lemma for poimir 37182, 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 5993 . . . 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 12256 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
4 npcan1 11667 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53, 4syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
62nnzd 12613 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
7 peano2zm 12633 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8 uzid 12865 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9 peano2uz 12913 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
106, 7, 8, 94syl 19 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
115, 10eqeltrrd 2826 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
12 fzss2 13571 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
1513, 14sseldd 3973 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
16 fzp1elp1 13584 . . . . . . . . . 10 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
185oveq2d 7431 . . . . . . . . 9 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
1917, 18eleqtrd 2827 . . . . . . . 8 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
2015, 19prssd 4821 . . . . . . 7 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
21 undif 4477 . . . . . . 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 5979 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) ↾ (1...𝑁)))
24 poimirlem9.3 . . . . . . . 8 (𝜑𝑈𝑆)
25 elrabi 3669 . . . . . . . . 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 2843 . . . . . . . 8 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28 xp1st 8021 . . . . . . . 8 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29 xp2nd 8022 . . . . . . . 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 6904 . . . . . . . 8 (2nd ‘(1st𝑈)) ∈ V
32 f1oeq1 6821 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3331, 32elab 3660 . . . . . . 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 6834 . . . . . 6 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)) Fn (1...𝑁))
36 fnresdm 6668 . . . . . 6 ((2nd ‘(1st𝑈)) Fn (1...𝑁) → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3734, 35, 363syl 18 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3823, 37eqtrd 2765 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
391, 38eqtr3id 2779 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
40 2lt3 12412 . . . . . 6 2 < 3
41 2re 12314 . . . . . . 7 2 ∈ ℝ
42 3re 12320 . . . . . . 7 3 ∈ ℝ
4341, 42ltnlei 11363 . . . . . 6 (2 < 3 ↔ ¬ 3 ≤ 2)
4440, 43mpbi 229 . . . . 5 ¬ 3 ≤ 2
45 df-pr 4627 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
4645coeq2i 5857 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
47 coundi 6246 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
4846, 47eqtri 2753 . . . . . . . . . 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 3669 . . . . . . . . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52 xp1st 8021 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53 xp2nd 8022 . . . . . . . . . . . . . . . . . . . 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 6904 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
56 f1oeq1 6821 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
5755, 56elab 3660 . . . . . . . . . . . . . . . . . . 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 6832 . . . . . . . . . . . . . . . . . 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 4808 . . . . . . . . . . . . . . . . 17 (𝜑 → {((2nd𝑇) + 1)} ⊆ (1...𝑁))
62 f1ores 6847 . . . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
64 f1of 6833 . . . . . . . . . . . . . . . 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 6834 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
6758, 66syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
68 fnsnfv 6971 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
6967, 19, 68syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
7069feq3d 6703 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} ↔ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)})))
7165, 70mpbird 256 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
72 eqid 2725 . . . . . . . . . . . . . . 15 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}
73 fvex 6904 . . . . . . . . . . . . . . . 16 (2nd𝑇) ∈ V
74 ovex 7448 . . . . . . . . . . . . . . . 16 ((2nd𝑇) + 1) ∈ V
7573, 74fsn 7139 . . . . . . . . . . . . . . 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 6744 . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}):{(2nd𝑇)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
79 fvex 6904 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V
8079fconst2 7212 . . . . . . . . . . . . 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 7145 . . . . . . . . . . . 12 ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
8381, 82eqtrdi 2781 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
8483uneq1d 4155 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
8548, 84eqtrid 2777 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
86 elfznn 13560 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
8714, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) ∈ ℕ)
8887nnred 12255 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) ∈ ℝ)
8988ltp1d 12172 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
9088, 89ltned 11378 . . . . . . . . . . . . . 14 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
9190necomd 2986 . . . . . . . . . . . . 13 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
92 f1veqaeq 7262 . . . . . . . . . . . . . . 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 835 . . . . . . . . . . . . . 14 (𝜑 → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9493necon3d 2951 . . . . . . . . . . . . 13 (𝜑 → (((2nd𝑇) + 1) ≠ (2nd𝑇) → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9591, 94mpd 15 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9695neneqd 2935 . . . . . . . . . . 11 (𝜑 → ¬ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9773, 79opth 5472 . . . . . . . . . . . 12 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩ ↔ ((2nd𝑇) = (2nd𝑇) ∧ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9897simprbi 495 . . . . . . . . . . 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 2935 . . . . . . . . . . 11 (𝜑 → ¬ (2nd𝑇) = ((2nd𝑇) + 1))
10173, 79opth1 5471 . . . . . . . . . . 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 5460 . . . . . . . . . . . . . . 15 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ V
104103snid 4660 . . . . . . . . . . . . . 14 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
105 elun1 4170 . . . . . . . . . . . . . 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 2814 . . . . . . . . . . . . 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 4648 . . . . . . . . . . . . 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 987 . . . . . . . . . . . . 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 274 . . . . . . . . . . . 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 2960 . . . . . . . . . 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 582 . . . . . . . . 9 (𝜑 → ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11585, 114eqnetrd 2998 . . . . . . . 8 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
116 fnressn 7162 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
11767, 15, 116syl2anc 582 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
118 fnressn 7162 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11967, 19, 118syl2anc 582 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
120117, 119uneq12d 4157 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}))
121 df-pr 4627 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
122121reseq2i 5976 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
123 resundi 5993 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
124122, 123eqtri 2753 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
125 df-pr 4627 . . . . . . . . . 10 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
126120, 124, 1253eqtr4g 2790 . . . . . . . . 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 37157 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
129 uneq12 4151 . . . . . . . . . . . . . 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 5993 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
13122reseq2d 5979 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ (1...𝑁)))
132 fnresdm 6668 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) Fn (1...𝑁) → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
13358, 66, 1323syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
134131, 133eqtrd 2765 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
135130, 134eqtr3id 2779 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
13639, 135eqeq12d 2741 . . . . . . . . . . . . . 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 692 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
139138necon3d 2951 . . . . . . . . . . 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 2986 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
142126, 141eqnetrrd 2999 . . . . . . . 8 (𝜑 → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
143 prex 5428 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
14455, 143coex 7934 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∈ V
145 prex 5428 . . . . . . . . . . 11 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∈ V
14631resex 6028 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V
147 hashtpg 14476 . . . . . . . . . . 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 582 . . . . . . 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 5428 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ V
153 prex 5428 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ V
154152, 153mapval 8853 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}
155 prfi 9344 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin
156 prfi 9344 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin
157 mapfi 9370 . . . . . . . . . . . . 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 690 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
159154, 158eqeltrri 2822 . . . . . . . . . . 11 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
160 f1of 6833 . . . . . . . . . . . 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 4055 . . . . . . . . . . 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 9194 . . . . . . . . . . 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 690 . . . . . . . . . 10 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
16419, 15prssd 4821 . . . . . . . . . . . . . . 15 (𝜑 → {((2nd𝑇) + 1), (2nd𝑇)} ⊆ (1...𝑁))
165 f1ores 6847 . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}):{((2nd𝑇) + 1), (2nd𝑇)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}))
167 fnimapr 6976 . . . . . . . . . . . . . . . 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 6830 . . . . . . . . . . . . . 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 6878 . . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . 13 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
174 f1oco 6856 . . . . . . . . . . . . 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 582 . . . . . . . . . . . 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 6221 . . . . . . . . . . . . . . 15 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
17773, 74, 176mp2an 690 . . . . . . . . . . . . . 14 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)}
178177eqimssi 4033 . . . . . . . . . . . . 13 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ {((2nd𝑇) + 1), (2nd𝑇)}
179 cores 6248 . . . . . . . . . . . . 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 6821 . . . . . . . . . . . . 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 2986 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
184 fvex 6904 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V
185 f1oprg 6878 . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . 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 582 . . . . . . . . . . . 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 4732 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}
189 f1oeq3 6823 . . . . . . . . . . . . 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 6832 . . . . . . . . . . . . . 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 6847 . . . . . . . . . . . . 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 582 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
196 dff1o3 6839 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
197196simprbi 495 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
198 imadif 6631 . . . . . . . . . . . . . . . 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 6840 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
201 foima 6810 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
20234, 200, 2013syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
203 f1ofo 6840 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
204 foima 6810 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
20558, 203, 2043syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
206202, 205eqtr4d 2768 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ (1...𝑁)))
207128rneqd 5934 . . . . . . . . . . . . . . . . 17 (𝜑 → ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
208 df-ima 5685 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
209 df-ima 5685 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
210207, 208, 2093eqtr4g 2790 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
211206, 210difeq12d 4115 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
212 dff1o3 6839 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
213212simprbi 495 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
214 imadif 6631 . . . . . . . . . . . . . . . . 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 4209 . . . . . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = {(2nd𝑇), ((2nd𝑇) + 1)})
220219imaeq2d 6058 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
221215, 220eqtr3d 2767 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
222199, 211, 2213eqtrd 2769 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
223219imaeq2d 6058 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
224 fnimapr 6976 . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
227222, 223, 2263eqtr3d 2773 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
228227f1oeq3d 6830 . . . . . . . . . . . 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 4052 . . . . . . . . . . . 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 6821 . . . . . . . . . . . . 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 6821 . . . . . . . . . . . . 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 6821 . . . . . . . . . . . . 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 4705 . . . . . . . . . . . 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 274 . . . . . . . . . . 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 14398 . . . . . . . . . 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 585 . . . . . . . . 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 9002 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}
240 hashprg 14384 . . . . . . . . . . . . . . . 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 690 . . . . . . . . . . . . . . 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 14384 . . . . . . . . . . . . . . . 16 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2))
24473, 74, 243mp2an 690 . . . . . . . . . . . . . . 15 ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
24590, 244sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
246242, 245eqtr4d 2768 . . . . . . . . . . . . 13 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
247 hashen 14336 . . . . . . . . . . . . . 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 690 . . . . . . . . . . . . 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 14443 . . . . . . . . . . . 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 585 . . . . . . . . . . 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 8853 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
253 mapfi 9370 . . . . . . . . . . . . . . 15 (({(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin)
254156, 156, 253mp2an 690 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
255252, 254eqeltrri 2822 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
256 f1of 6833 . . . . . . . . . . . . . 14 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)})
257256ss2abi 4055 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
258 ssfi 9194 . . . . . . . . . . . . 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 690 . . . . . . . . . . . 12 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
260 hashen 14336 . . . . . . . . . . . 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 690 . . . . . . . . . . 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 14449 . . . . . . . . . . . 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 6895 . . . . . . . . . . . 12 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = (!‘2))
266 fac2 14268 . . . . . . . . . . . 12 (!‘2) = 2
267265, 266eqtrdi 2781 . . . . . . . . . . 11 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = 2)
268264, 267eqtrid 2777 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = 2)
269262, 268eqtrd 2765 . . . . . . . . 9 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = 2)
270238, 269breqtrd 5169 . . . . . . . 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 5146 . . . . . . . 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 2948 . . . . 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 6263 . . . . 5 ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
277128, 276eqtr4di 2783 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
278275, 277uneq12d 4157 . . 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 2767 . 2 (𝜑 → (2nd ‘(1st𝑈)) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
280 coundi 6246 . 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 2783 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 394  wo 845  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wne 2930  wral 3051  {crab 3419  Vcvv 3463  csb 3885  cdif 3937  cun 3938  cin 3939  wss 3940  ifcif 4524  {csn 4624  {cpr 4626  {ctp 4628  cop 4630   class class class wbr 5143  cmpt 5226   I cid 5569   × cxp 5670  ccnv 5671  ran crn 5673  cres 5674  cima 5675  ccom 5676  Fun wfun 6536   Fn wfn 6537  wf 6538  1-1wf1 6539  ontowfo 6540  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7415  f cof 7679  1st c1st 7987  2nd c2nd 7988  m cmap 8841  cen 8957  Fincfn 8960  cc 11134  0cc0 11136  1c1 11137   + caddc 11139   < clt 11276  cle 11277  cmin 11472  cn 12240  2c2 12295  3c3 12296  cz 12586  cuz 12850  ...cfz 13514  ..^cfzo 13657  !cfa 14262  chash 14319
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 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  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 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7681  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-oadd 8487  df-er 8721  df-map 8843  df-pm 8844  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-dju 9922  df-card 9960  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-n0 12501  df-xnn0 12573  df-z 12587  df-uz 12851  df-fz 13515  df-fzo 13658  df-seq 13997  df-fac 14263  df-bc 14292  df-hash 14320
This theorem is referenced by:  poimirlem22  37171
  Copyright terms: Public domain W3C validator