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 34783
Description: Lemma for poimir 34807, 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 5861 . . . 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 11643 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
4 npcan1 11054 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53, 4syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
62nnzd 12075 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
7 peano2zm 12014 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8 uzid 12247 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9 peano2uz 12290 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
106, 7, 8, 94syl 19 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
115, 10eqeltrrd 2914 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
12 fzss2 12937 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
1513, 14sseldd 3967 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
16 fzp1elp1 12950 . . . . . . . . . 10 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
185oveq2d 7161 . . . . . . . . 9 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
1917, 18eleqtrd 2915 . . . . . . . 8 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
2015, 19prssd 4749 . . . . . . 7 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
21 undif 4428 . . . . . . 7 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
2220, 21sylib 219 . . . . . 6 (𝜑 → ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
2322reseq2d 5847 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) ↾ (1...𝑁)))
24 poimirlem9.3 . . . . . . . 8 (𝜑𝑈𝑆)
25 elrabi 3674 . . . . . . . . 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 2931 . . . . . . . 8 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28 xp1st 7712 . . . . . . . 8 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29 xp2nd 7713 . . . . . . . 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 6677 . . . . . . . 8 (2nd ‘(1st𝑈)) ∈ V
32 f1oeq1 6598 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3331, 32elab 3666 . . . . . . 7 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
3430, 33sylib 219 . . . . . 6 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
35 f1ofn 6610 . . . . . 6 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)) Fn (1...𝑁))
36 fnresdm 6460 . . . . . 6 ((2nd ‘(1st𝑈)) Fn (1...𝑁) → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3734, 35, 363syl 18 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3823, 37eqtrd 2856 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
391, 38syl5eqr 2870 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
40 2lt3 11798 . . . . . 6 2 < 3
41 2re 11700 . . . . . . 7 2 ∈ ℝ
42 3re 11706 . . . . . . 7 3 ∈ ℝ
4341, 42ltnlei 10750 . . . . . 6 (2 < 3 ↔ ¬ 3 ≤ 2)
4440, 43mpbi 231 . . . . 5 ¬ 3 ≤ 2
45 df-pr 4562 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
4645coeq2i 5725 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
47 coundi 6094 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
4846, 47eqtri 2844 . . . . . . . . . 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 3674 . . . . . . . . . . . . . . . . . . . . 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 2931 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52 xp1st 7712 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53 xp2nd 7713 . . . . . . . . . . . . . . . . . . . 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 6677 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
56 f1oeq1 6598 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
5755, 56elab 3666 . . . . . . . . . . . . . . . . . . 19 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
5854, 57sylib 219 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
59 f1of1 6608 . . . . . . . . . . . . . . . . . 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 4736 . . . . . . . . . . . . . . . . 17 (𝜑 → {((2nd𝑇) + 1)} ⊆ (1...𝑁))
62 f1ores 6623 . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
64 f1of 6609 . . . . . . . . . . . . . . . 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 6610 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
6758, 66syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
68 fnsnfv 6737 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
6967, 19, 68syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)}))
7069feq3d 6495 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} ↔ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1)})))
7165, 70mpbird 258 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}):{((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
72 eqid 2821 . . . . . . . . . . . . . . 15 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}
73 fvex 6677 . . . . . . . . . . . . . . . 16 (2nd𝑇) ∈ V
74 ovex 7178 . . . . . . . . . . . . . . . 16 ((2nd𝑇) + 1) ∈ V
7573, 74fsn 6890 . . . . . . . . . . . . . . 15 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}:{(2nd𝑇)}⟶{((2nd𝑇) + 1)} ↔ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩})
7672, 75mpbir 232 . . . . . . . . . . . . . 14 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}:{(2nd𝑇)}⟶{((2nd𝑇) + 1)}
77 fco2 6527 . . . . . . . . . . . . . 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 586 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}):{(2nd𝑇)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
79 fvex 6677 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V
8079fconst2 6960 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}):{(2nd𝑇)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} ↔ ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}))
8178, 80sylib 219 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}))
8273, 79xpsn 6896 . . . . . . . . . . . 12 ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
8381, 82syl6eq 2872 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
8483uneq1d 4137 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
8548, 84syl5eq 2868 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
86 elfznn 12926 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
8714, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) ∈ ℕ)
8887nnred 11642 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) ∈ ℝ)
8988ltp1d 11559 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
9088, 89ltned 10765 . . . . . . . . . . . . . 14 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
9190necomd 3071 . . . . . . . . . . . . 13 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
92 f1veqaeq 7006 . . . . . . . . . . . . . . 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 832 . . . . . . . . . . . . . 14 (𝜑 → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9493necon3d 3037 . . . . . . . . . . . . 13 (𝜑 → (((2nd𝑇) + 1) ≠ (2nd𝑇) → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9591, 94mpd 15 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9695neneqd 3021 . . . . . . . . . . 11 (𝜑 → ¬ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9773, 79opth 5360 . . . . . . . . . . . 12 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩ ↔ ((2nd𝑇) = (2nd𝑇) ∧ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9897simprbi 497 . . . . . . . . . . 11 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩ → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9996, 98nsyl 142 . . . . . . . . . 10 (𝜑 → ¬ ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩)
10090neneqd 3021 . . . . . . . . . . 11 (𝜑 → ¬ (2nd𝑇) = ((2nd𝑇) + 1))
10173, 79opth1 5359 . . . . . . . . . . 11 (⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ → (2nd𝑇) = ((2nd𝑇) + 1))
102100, 101nsyl 142 . . . . . . . . . 10 (𝜑 → ¬ ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩)
103 opex 5348 . . . . . . . . . . . . . . 15 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ V
104103snid 4593 . . . . . . . . . . . . . 14 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
105 elun1 4151 . . . . . . . . . . . . . 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 2901 . . . . . . . . . . . . 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 234 . . . . . . . . . . . 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 4582 . . . . . . . . . . . . 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 983 . . . . . . . . . . . . 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 276 . . . . . . . . . . . 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 219 . . . . . . . . . . 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 3045 . . . . . . . . . 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 584 . . . . . . . . 9 (𝜑 → ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11585, 114eqnetrd 3083 . . . . . . . 8 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
116 fnressn 6913 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
11767, 15, 116syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩})
118 fnressn 6913 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
11967, 19, 118syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}) = {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
120117, 119uneq12d 4139 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}))
121 df-pr 4562 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
122121reseq2i 5844 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
123 resundi 5861 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
124122, 123eqtri 2844 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
125 df-pr 4562 . . . . . . . . . 10 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
126120, 124, 1253eqtr4g 2881 . . . . . . . . 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 34782 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
129 uneq12 4133 . . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
13122reseq2d 5847 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ (1...𝑁)))
132 fnresdm 6460 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) Fn (1...𝑁) → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
13358, 66, 1323syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
134131, 133eqtrd 2856 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
135130, 134syl5eqr 2870 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
13639, 135eqeq12d 2837 . . . . . . . . . . . . . 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, 136syl5ib 245 . . . . . . . . . . . . 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 690 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
139138necon3d 3037 . . . . . . . . . . 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 3071 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
142126, 141eqnetrrd 3084 . . . . . . . 8 (𝜑 → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
143 prex 5324 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
14455, 143coex 7623 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∈ V
145 prex 5324 . . . . . . . . . . 11 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∈ V
14631resex 5893 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V
147 hashtpg 13833 . . . . . . . . . . 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 1452 . . . . . . . . . 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 217 . . . . . . . . 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 1113 . . . . . . . 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 584 . . . . . . 7 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) → (♯‘{((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}), {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}, ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)})}) = 3))
152 prex 5324 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ V
153 prex 5324 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ V
154152, 153mapval 8408 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}
155 prfi 8782 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin
156 prfi 8782 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin
157 mapfi 8809 . . . . . . . . . . . . 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 688 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
159154, 158eqeltrri 2910 . . . . . . . . . . 11 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
160 f1of 6609 . . . . . . . . . . . 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 4042 . . . . . . . . . . 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 8727 . . . . . . . . . . 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 688 . . . . . . . . . 10 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
16419, 15prssd 4749 . . . . . . . . . . . . . . 15 (𝜑 → {((2nd𝑇) + 1), (2nd𝑇)} ⊆ (1...𝑁))
165 f1ores 6623 . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}):{((2nd𝑇) + 1), (2nd𝑇)}–1-1-onto→((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}))
167 fnimapr 6741 . . . . . . . . . . . . . . . 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 1363 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
169168f1oeq3d 6606 . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}):{((2nd𝑇) + 1), (2nd𝑇)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
171 f1oprg 6653 . . . . . . . . . . . . . . 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 689 . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . 13 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
174 f1oco 6631 . . . . . . . . . . . . 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 584 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1), (2nd𝑇)}) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
176 rnpropg 6073 . . . . . . . . . . . . . . 15 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
17773, 74, 176mp2an 688 . . . . . . . . . . . . . 14 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)}
178177eqimssi 4024 . . . . . . . . . . . . 13 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ {((2nd𝑇) + 1), (2nd𝑇)}
179 cores 6096 . . . . . . . . . . . . 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 6598 . . . . . . . . . . . . 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 219 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
18395necomd 3071 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
184 fvex 6677 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V
185 f1oprg 6653 . . . . . . . . . . . . . 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 689 . . . . . . . . . . . . 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 584 . . . . . . . . . . . 12 (𝜑 → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
188 prcom 4662 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}
189 f1oeq3 6600 . . . . . . . . . . . . 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 219 . . . . . . . . . . 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 6608 . . . . . . . . . . . . . 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 6623 . . . . . . . . . . . . 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 584 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
196 dff1o3 6615 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
197196simprbi 497 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
198 imadif 6432 . . . . . . . . . . . . . . . 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 6616 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
201 foima 6589 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
20234, 200, 2013syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
203 f1ofo 6616 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
204 foima 6589 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
20558, 203, 2043syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
206202, 205eqtr4d 2859 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ (1...𝑁)))
207128rneqd 5802 . . . . . . . . . . . . . . . . 17 (𝜑 → ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
208 df-ima 5562 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
209 df-ima 5562 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
210207, 208, 2093eqtr4g 2881 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
211206, 210difeq12d 4099 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
212 dff1o3 6615 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
213212simprbi 497 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
214 imadif 6432 . . . . . . . . . . . . . . . . 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 4243 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
217 sseqin2 4191 . . . . . . . . . . . . . . . . . . 19 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
21820, 217sylib 219 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
219216, 218syl5eqr 2870 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = {(2nd𝑇), ((2nd𝑇) + 1)})
220219imaeq2d 5923 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
221215, 220eqtr3d 2858 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
222199, 211, 2213eqtrd 2860 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
223219imaeq2d 5923 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
224 fnimapr 6741 . . . . . . . . . . . . . . . 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 1363 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
226225, 188syl6eq 2872 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
227222, 223, 2263eqtr3d 2864 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
228227f1oeq3d 6606 . . . . . . . . . . . 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 233 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}):{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
230 ssabral 4041 . . . . . . . . . . . 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 6598 . . . . . . . . . . . . 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 6598 . . . . . . . . . . . . 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 6598 . . . . . . . . . . . . 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 4635 . . . . . . . . . . . 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 276 . . . . . . . . . . 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 1335 . . . . . . . . . 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 13760 . . . . . . . . . 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 587 . . . . . . . . 9 (𝜑 → (♯‘{((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}), {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}, ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)})}) ≤ (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}))
239153enref 8531 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}
240 hashprg 13746 . . . . . . . . . . . . . . . 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 688 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ↔ (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
24295, 241sylib 219 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
243 hashprg 13746 . . . . . . . . . . . . . . . 16 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2))
24473, 74, 243mp2an 688 . . . . . . . . . . . . . . 15 ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
24590, 244sylib 219 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
246242, 245eqtr4d 2859 . . . . . . . . . . . . 13 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
247 hashen 13697 . . . . . . . . . . . . . 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 688 . . . . . . . . . . . . 13 ((♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) ↔ {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
249246, 248sylib 219 . . . . . . . . . . . 12 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
250 hashfacen 13802 . . . . . . . . . . . 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 587 . . . . . . . . . . 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 8408 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
253 mapfi 8809 . . . . . . . . . . . . . . 15 (({(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin)
254156, 156, 253mp2an 688 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
255252, 254eqeltrri 2910 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
256 f1of 6609 . . . . . . . . . . . . . 14 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)})
257256ss2abi 4042 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
258 ssfi 8727 . . . . . . . . . . . . 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 688 . . . . . . . . . . . 12 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
260 hashen 13697 . . . . . . . . . . . 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 688 . . . . . . . . . . 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 235 . . . . . . . . . 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 13806 . . . . . . . . . . . 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 6668 . . . . . . . . . . . 12 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = (!‘2))
266 fac2 13629 . . . . . . . . . . . 12 (!‘2) = 2
267265, 266syl6eq 2872 . . . . . . . . . . 11 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = 2)
268264, 267syl5eq 2868 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = 2)
269262, 268eqtrd 2856 . . . . . . . . 9 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = 2)
270238, 269breqtrd 5084 . . . . . . . 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 5061 . . . . . . . 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 246 . . . . . . 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 3034 . . . . 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 6111 . . . . 5 ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
277128, 276syl6eqr 2874 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
278275, 277uneq12d 4139 . . 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 2858 . 2 (𝜑 → (2nd ‘(1st𝑈)) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
280 coundi 6094 . 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, 280syl6eqr 2874 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 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  {cab 2799  wne 3016  wral 3138  {crab 3142  Vcvv 3495  csb 3882  cdif 3932  cun 3933  cin 3934  wss 3935  ifcif 4465  {csn 4559  {cpr 4561  {ctp 4563  cop 4565   class class class wbr 5058  cmpt 5138   I cid 5453   × cxp 5547  ccnv 5548  ran crn 5550  cres 5551  cima 5552  ccom 5553  Fun wfun 6343   Fn wfn 6344  wf 6345  1-1wf1 6346  ontowfo 6347  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  f cof 7396  1st c1st 7678  2nd c2nd 7679  m cmap 8396  cen 8495  Fincfn 8498  cc 10524  0cc0 10526  1c1 10527   + caddc 10529   < clt 10664  cle 10665  cmin 10859  cn 11627  2c2 11681  3c3 11682  cz 11970  cuz 12232  ...cfz 12882  ..^cfzo 13023  !cfa 13623  chash 13680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-dju 9319  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-n0 11887  df-xnn0 11957  df-z 11971  df-uz 12233  df-fz 12883  df-fzo 13024  df-seq 13360  df-fac 13624  df-bc 13653  df-hash 13681
This theorem is referenced by:  poimirlem22  34796
  Copyright terms: Public domain W3C validator