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 37330
Description: Lemma for poimir 37354, 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 6003 . . . 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 12280 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
4 npcan1 11689 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53, 4syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
62nnzd 12637 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
7 peano2zm 12657 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8 uzid 12889 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9 peano2uz 12937 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
106, 7, 8, 94syl 19 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
115, 10eqeltrrd 2827 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
12 fzss2 13595 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
1513, 14sseldd 3980 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
16 fzp1elp1 13608 . . . . . . . . . 10 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
185oveq2d 7440 . . . . . . . . 9 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
1917, 18eleqtrd 2828 . . . . . . . 8 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
2015, 19prssd 4831 . . . . . . 7 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
21 undif 4486 . . . . . . 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 5989 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) ↾ (1...𝑁)))
24 poimirlem9.3 . . . . . . . 8 (𝜑𝑈𝑆)
25 elrabi 3675 . . . . . . . . 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 2844 . . . . . . . 8 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28 xp1st 8035 . . . . . . . 8 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29 xp2nd 8036 . . . . . . . 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 6914 . . . . . . . 8 (2nd ‘(1st𝑈)) ∈ V
32 f1oeq1 6831 . . . . . . . 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 217 . . . . . 6 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
35 f1ofn 6844 . . . . . 6 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)) Fn (1...𝑁))
36 fnresdm 6680 . . . . . 6 ((2nd ‘(1st𝑈)) Fn (1...𝑁) → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3734, 35, 363syl 18 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3823, 37eqtrd 2766 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
391, 38eqtr3id 2780 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
40 2lt3 12436 . . . . . 6 2 < 3
41 2re 12338 . . . . . . 7 2 ∈ ℝ
42 3re 12344 . . . . . . 7 3 ∈ ℝ
4341, 42ltnlei 11385 . . . . . 6 (2 < 3 ↔ ¬ 3 ≤ 2)
4440, 43mpbi 229 . . . . 5 ¬ 3 ≤ 2
45 df-pr 4636 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
4645coeq2i 5867 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
47 coundi 6258 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
4846, 47eqtri 2754 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
49 poimirlem9.1 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇𝑆)
50 elrabi 3675 . . . . . . . . . . . . . . . . . . . . 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 2844 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52 xp1st 8035 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53 xp2nd 8036 . . . . . . . . . . . . . . . . . . . 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 6914 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
56 f1oeq1 6831 . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
59 f1of1 6842 . . . . . . . . . . . . . . . . . 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 4818 . . . . . . . . . . . . . . . . 17 (𝜑 → {((2nd𝑇) + 1)} ⊆ (1...𝑁))
62 f1ores 6857 . . . . . . . . . . . . . . . . 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 6843 . . . . . . . . . . . . . . . 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 6844 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
6758, 66syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
68 fnsnfv 6981 . . . . . . . . . . . . . . . . 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 6715 . . . . . . . . . . . . . . 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 2726 . . . . . . . . . . . . . . 15 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}
73 fvex 6914 . . . . . . . . . . . . . . . 16 (2nd𝑇) ∈ V
74 ovex 7457 . . . . . . . . . . . . . . . 16 ((2nd𝑇) + 1) ∈ V
7573, 74fsn 7149 . . . . . . . . . . . . . . 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 6755 . . . . . . . . . . . . . 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 6914 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V
8079fconst2 7222 . . . . . . . . . . . . 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 7155 . . . . . . . . . . . 12 ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
8381, 82eqtrdi 2782 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
8483uneq1d 4162 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
8548, 84eqtrid 2778 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
86 elfznn 13584 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
8714, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) ∈ ℕ)
8887nnred 12279 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) ∈ ℝ)
8988ltp1d 12196 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
9088, 89ltned 11400 . . . . . . . . . . . . . 14 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
9190necomd 2986 . . . . . . . . . . . . 13 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
92 f1veqaeq 7272 . . . . . . . . . . . . . . 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 5482 . . . . . . . . . . . 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 5481 . . . . . . . . . . 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 5470 . . . . . . . . . . . . . . 15 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ V
104103snid 4669 . . . . . . . . . . . . . 14 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
105 elun1 4177 . . . . . . . . . . . . . 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 2815 . . . . . . . . . . . . 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 4657 . . . . . . . . . . . . 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 7172 . . . . . . . . . . . 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 7172 . . . . . . . . . . . 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 4164 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}))
121 df-pr 4636 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
122121reseq2i 5986 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
123 resundi 6003 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
124122, 123eqtri 2754 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
125 df-pr 4636 . . . . . . . . . 10 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
126120, 124, 1253eqtr4g 2791 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
127 poimirlem9.4 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑈)) ≠ (2nd ‘(1st𝑇)))
1282, 26, 49, 14, 24poimirlem8 37329 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
129 uneq12 4158 . . . . . . . . . . . . . 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 6003 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
13122reseq2d 5989 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ (1...𝑁)))
132 fnresdm 6680 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) Fn (1...𝑁) → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
13358, 66, 1323syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
134131, 133eqtrd 2766 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
135130, 134eqtr3id 2780 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
13639, 135eqeq12d 2742 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) ↔ (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
137129, 136imbitrid 243 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∧ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
138128, 137mpan2d 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 5438 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
14455, 143coex 7943 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∈ V
145 prex 5438 . . . . . . . . . . 11 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∈ V
14631resex 6038 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V
147 hashtpg 14504 . . . . . . . . . . 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 1458 . . . . . . . . . 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 5438 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ V
153 prex 5438 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ V
154152, 153mapval 8867 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}
155 prfi 9365 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin
156 prfi 9365 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin
157 mapfi 9392 . . . . . . . . . . . . 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 2823 . . . . . . . . . . 11 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
160 f1of 6843 . . . . . . . . . . . 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 4062 . . . . . . . . . . 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 9211 . . . . . . . . . . 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 4831 . . . . . . . . . . . . . . 15 (𝜑 → {((2nd𝑇) + 1), (2nd𝑇)} ⊆ (1...𝑁))
165 f1ores 6857 . . . . . . . . . . . . . . 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 6986 . . . . . . . . . . . . . . . 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 6840 . . . . . . . . . . . . . 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 6888 . . . . . . . . . . . . . . 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 6866 . . . . . . . . . . . . 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 6233 . . . . . . . . . . . . . . 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 4040 . . . . . . . . . . . . 13 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ {((2nd𝑇) + 1), (2nd𝑇)}
179 cores 6260 . . . . . . . . . . . . 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 6831 . . . . . . . . . . . . 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 6914 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V
185 f1oprg 6888 . . . . . . . . . . . . . 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 4741 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}
189 f1oeq3 6833 . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . 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 6857 . . . . . . . . . . . . 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 6849 . . . . . . . . . . . . . . . . 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 6643 . . . . . . . . . . . . . . . 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 6850 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
201 foima 6820 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
20234, 200, 2013syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
203 f1ofo 6850 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
204 foima 6820 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
20558, 203, 2043syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
206202, 205eqtr4d 2769 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ (1...𝑁)))
207128rneqd 5944 . . . . . . . . . . . . . . . . 17 (𝜑 → ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
208 df-ima 5695 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
209 df-ima 5695 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
210207, 208, 2093eqtr4g 2791 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
211206, 210difeq12d 4122 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
212 dff1o3 6849 . . . . . . . . . . . . . . . . . 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 6643 . . . . . . . . . . . . . . . . 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 4269 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
217 sseqin2 4216 . . . . . . . . . . . . . . . . . . 19 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
21820, 217sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = {(2nd𝑇), ((2nd𝑇) + 1)})
219216, 218eqtr3id 2780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = {(2nd𝑇), ((2nd𝑇) + 1)})
220219imaeq2d 6069 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
221215, 220eqtr3d 2768 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
222199, 211, 2213eqtrd 2770 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
223219imaeq2d 6069 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
224 fnimapr 6986 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
22567, 15, 19, 224syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
226225, 188eqtrdi 2782 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
227222, 223, 2263eqtr3d 2774 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
228227f1oeq3d 6840 . . . . . . . . . . . 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 4059 . . . . . . . . . . . 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 6831 . . . . . . . . . . . . 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 6831 . . . . . . . . . . . . 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 6831 . . . . . . . . . . . . 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 4714 . . . . . . . . . . . 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 14426 . . . . . . . . . 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 9016 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}
240 hashprg 14412 . . . . . . . . . . . . . . . 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 14412 . . . . . . . . . . . . . . . 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 2769 . . . . . . . . . . . . 13 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
247 hashen 14364 . . . . . . . . . . . . . 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 14471 . . . . . . . . . . . 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 8867 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
253 mapfi 9392 . . . . . . . . . . . . . . 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 2823 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
256 f1of 6843 . . . . . . . . . . . . . 14 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)})
257256ss2abi 4062 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
258 ssfi 9211 . . . . . . . . . . . . 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 14364 . . . . . . . . . . . 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 14477 . . . . . . . . . . . 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 6905 . . . . . . . . . . . 12 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = (!‘2))
266 fac2 14296 . . . . . . . . . . . 12 (!‘2) = 2
267265, 266eqtrdi 2782 . . . . . . . . . . 11 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = 2)
268264, 267eqtrid 2778 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = 2)
269262, 268eqtrd 2766 . . . . . . . . 9 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = 2)
270238, 269breqtrd 5179 . . . . . . . 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 5156 . . . . . . . 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 6275 . . . . 5 ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
277128, 276eqtr4di 2784 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
278275, 277uneq12d 4164 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
27939, 278eqtr3d 2768 . 2 (𝜑 → (2nd ‘(1st𝑈)) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
280 coundi 6258 . 2 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
281279, 280eqtr4di 2784 1 (𝜑 → (2nd ‘(1st𝑈)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1534  wcel 2099  {cab 2703  wne 2930  wral 3051  {crab 3419  Vcvv 3462  csb 3892  cdif 3944  cun 3945  cin 3946  wss 3947  ifcif 4533  {csn 4633  {cpr 4635  {ctp 4637  cop 4639   class class class wbr 5153  cmpt 5236   I cid 5579   × cxp 5680  ccnv 5681  ran crn 5683  cres 5684  cima 5685  ccom 5686  Fun wfun 6548   Fn wfn 6549  wf 6550  1-1wf1 6551  ontowfo 6552  1-1-ontowf1o 6553  cfv 6554  (class class class)co 7424  f cof 7688  1st c1st 8001  2nd c2nd 8002  m cmap 8855  cen 8971  Fincfn 8974  cc 11156  0cc0 11158  1c1 11159   + caddc 11161   < clt 11298  cle 11299  cmin 11494  cn 12264  2c2 12319  3c3 12320  cz 12610  cuz 12874  ...cfz 13538  ..^cfzo 13681  !cfa 14290  chash 14347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-tp 4638  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-oadd 8500  df-er 8734  df-map 8857  df-pm 8858  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-dju 9944  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12597  df-z 12611  df-uz 12875  df-fz 13539  df-fzo 13682  df-seq 14022  df-fac 14291  df-bc 14320  df-hash 14348
This theorem is referenced by:  poimirlem22  37343
  Copyright terms: Public domain W3C validator