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 35772
Description: Lemma for poimir 35796, 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 5899 . . . 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 11977 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
4 npcan1 11388 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53, 4syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
62nnzd 12413 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
7 peano2zm 12351 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8 uzid 12585 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9 peano2uz 12629 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
106, 7, 8, 94syl 19 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
115, 10eqeltrrd 2840 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
12 fzss2 13284 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
14 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
1513, 14sseldd 3922 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
16 fzp1elp1 13297 . . . . . . . . . 10 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → ((2nd𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
185oveq2d 7284 . . . . . . . . 9 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
1917, 18eleqtrd 2841 . . . . . . . 8 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
2015, 19prssd 4756 . . . . . . 7 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
21 undif 4416 . . . . . . 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 5885 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) ↾ (1...𝑁)))
24 poimirlem9.3 . . . . . . . 8 (𝜑𝑈𝑆)
25 elrabi 3618 . . . . . . . . 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 2857 . . . . . . . 8 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
28 xp1st 7853 . . . . . . . 8 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
29 xp2nd 7854 . . . . . . . 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 6780 . . . . . . . 8 (2nd ‘(1st𝑈)) ∈ V
32 f1oeq1 6697 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3331, 32elab 3609 . . . . . . 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 6710 . . . . . 6 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)) Fn (1...𝑁))
36 fnresdm 6544 . . . . . 6 ((2nd ‘(1st𝑈)) Fn (1...𝑁) → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3734, 35, 363syl 18 . . . . 5 (𝜑 → ((2nd ‘(1st𝑈)) ↾ (1...𝑁)) = (2nd ‘(1st𝑈)))
3823, 37eqtrd 2778 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
391, 38eqtr3id 2792 . . 3 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑈)))
40 2lt3 12133 . . . . . 6 2 < 3
41 2re 12035 . . . . . . 7 2 ∈ ℝ
42 3re 12041 . . . . . . 7 3 ∈ ℝ
4341, 42ltnlei 11084 . . . . . 6 (2 < 3 ↔ ¬ 3 ≤ 2)
4440, 43mpbi 229 . . . . 5 ¬ 3 ≤ 2
45 df-pr 4565 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
4645coeq2i 5763 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
47 coundi 6145 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} ∪ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩}))
4846, 47eqtri 2766 . . . . . . . . . 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 3618 . . . . . . . . . . . . . . . . . . . . 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 2857 . . . . . . . . . . . . . . . . . . . 20 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
52 xp1st 7853 . . . . . . . . . . . . . . . . . . . 20 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
53 xp2nd 7854 . . . . . . . . . . . . . . . . . . . 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 6780 . . . . . . . . . . . . . . . . . . . 20 (2nd ‘(1st𝑇)) ∈ V
56 f1oeq1 6697 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
5755, 56elab 3609 . . . . . . . . . . . . . . . . . . 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 6708 . . . . . . . . . . . . . . . . . 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 4743 . . . . . . . . . . . . . . . . 17 (𝜑 → {((2nd𝑇) + 1)} ⊆ (1...𝑁))
62 f1ores 6723 . . . . . . . . . . . . . . . . 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 6709 . . . . . . . . . . . . . . . 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 6710 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
6758, 66syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
68 fnsnfv 6840 . . . . . . . . . . . . . . . . 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 6580 . . . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . 15 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩} = {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}
73 fvex 6780 . . . . . . . . . . . . . . . 16 (2nd𝑇) ∈ V
74 ovex 7301 . . . . . . . . . . . . . . . 16 ((2nd𝑇) + 1) ∈ V
7573, 74fsn 7000 . . . . . . . . . . . . . . 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 6620 . . . . . . . . . . . . . 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 6780 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V
8079fconst2 7073 . . . . . . . . . . . . 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 7006 . . . . . . . . . . . 12 ({(2nd𝑇)} × {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
8381, 82eqtrdi 2794 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) = {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
8483uneq1d 4096 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
8548, 84eqtrid 2790 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∪ ((2nd ‘(1st𝑇)) ∘ {⟨((2nd𝑇) + 1), (2nd𝑇)⟩})))
86 elfznn 13273 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
8714, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) ∈ ℕ)
8887nnred 11976 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) ∈ ℝ)
8988ltp1d 11893 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
9088, 89ltned 11099 . . . . . . . . . . . . . 14 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
9190necomd 2999 . . . . . . . . . . . . 13 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
92 f1veqaeq 7123 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ (((2nd𝑇) + 1) ∈ (1...𝑁) ∧ (2nd𝑇) ∈ (1...𝑁))) → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9360, 19, 15, 92syl12anc 834 . . . . . . . . . . . . . 14 (𝜑 → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)) → ((2nd𝑇) + 1) = (2nd𝑇)))
9493necon3d 2964 . . . . . . . . . . . . 13 (𝜑 → (((2nd𝑇) + 1) ≠ (2nd𝑇) → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇))))
9591, 94mpd 15 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9695neneqd 2948 . . . . . . . . . . 11 (𝜑 → ¬ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) = ((2nd ‘(1st𝑇))‘(2nd𝑇)))
9773, 79opth 5390 . . . . . . . . . . . 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 140 . . . . . . . . . 10 (𝜑 → ¬ ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ = ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩)
10090neneqd 2948 . . . . . . . . . . 11 (𝜑 → ¬ (2nd𝑇) = ((2nd𝑇) + 1))
10173, 79opth1 5389 . . . . . . . . . . 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 5378 . . . . . . . . . . . . . . 15 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ V
104103snid 4598 . . . . . . . . . . . . . 14 ⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩ ∈ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}
105 elun1 4110 . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . 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 4585 . . . . . . . . . . . . 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 2973 . . . . . . . . . 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 3011 . . . . . . . 8 (𝜑 → ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ≠ {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
116 fnressn 7023 . . . . . . . . . . . 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 7023 . . . . . . . . . . . 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 4098 . . . . . . . . . 10 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)})) = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}))
121 df-pr 4565 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
122121reseq2i 5882 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
123 resundi 5899 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
124122, 123eqtri 2766 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇)}) ∪ ((2nd ‘(1st𝑇)) ↾ {((2nd𝑇) + 1)}))
125 df-pr 4565 . . . . . . . . . 10 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} = ({⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩} ∪ {⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩})
126120, 124, 1253eqtr4g 2803 . . . . . . . . 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 35771 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
129 uneq12 4092 . . . . . . . . . . . . . 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 5899 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
13122reseq2d 5885 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ (1...𝑁)))
132 fnresdm 6544 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) Fn (1...𝑁) → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
13358, 66, 1323syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) ↾ (1...𝑁)) = (2nd ‘(1st𝑇)))
134131, 133eqtrd 2778 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) ↾ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
135130, 134eqtr3id 2792 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (2nd ‘(1st𝑇)))
13639, 135eqeq12d 2754 . . . . . . . . . . . . . 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 243 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∧ ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
138128, 137mpan2d 691 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) → (2nd ‘(1st𝑈)) = (2nd ‘(1st𝑇))))
139138necon3d 2964 . . . . . . . . . . 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 2999 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
142126, 141eqnetrrd 3012 . . . . . . . 8 (𝜑 → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ≠ ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}))
143 prex 5354 . . . . . . . . . . . 12 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
14455, 143coex 7768 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∈ V
145 prex 5354 . . . . . . . . . . 11 {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩} ∈ V
14631resex 5933 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)) ↾ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V
147 hashtpg 14187 . . . . . . . . . . 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 1460 . . . . . . . . . 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 1120 . . . . . . . 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 5354 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ V
153 prex 5354 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ V
154152, 153mapval 8615 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}
155 prfi 9077 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin
156 prfi 9077 . . . . . . . . . . . . 13 {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin
157 mapfi 9103 . . . . . . . . . . . . 13 (({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin)
158155, 156, 157mp2an 689 . . . . . . . . . . . 12 ({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
159154, 158eqeltrri 2836 . . . . . . . . . . 11 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
160 f1of 6709 . . . . . . . . . . . 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 4000 . . . . . . . . . . 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 8944 . . . . . . . . . . 11 (({𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin ∧ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) → {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin)
163159, 161, 162mp2an 689 . . . . . . . . . 10 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin
16419, 15prssd 4756 . . . . . . . . . . . . . . 15 (𝜑 → {((2nd𝑇) + 1), (2nd𝑇)} ⊆ (1...𝑁))
165 f1ores 6723 . . . . . . . . . . . . . . 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 6845 . . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {((2nd𝑇) + 1), (2nd𝑇)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
169168f1oeq3d 6706 . . . . . . . . . . . . . 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 6754 . . . . . . . . . . . . . . 15 ((((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) ∧ (((2nd𝑇) + 1) ∈ V ∧ (2nd𝑇) ∈ V)) → (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≠ (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)}))
17273, 74, 74, 73, 171mp4an 690 . . . . . . . . . . . . . 14 (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≠ (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
17390, 91, 172syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
174 f1oco 6732 . . . . . . . . . . . . 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 6119 . . . . . . . . . . . . . . 15 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
17773, 74, 176mp2an 689 . . . . . . . . . . . . . 14 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)}
178177eqimssi 3979 . . . . . . . . . . . . 13 ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ {((2nd𝑇) + 1), (2nd𝑇)}
179 cores 6147 . . . . . . . . . . . . 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 6697 . . . . . . . . . . . . 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 2999 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)))
184 fvex 6780 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V
185 f1oprg 6754 . . . . . . . . . . . . . 14 ((((2nd𝑇) ∈ V ∧ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V) ∧ (((2nd𝑇) + 1) ∈ V ∧ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V)) → (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))) → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))}))
18673, 184, 74, 79, 185mp4an 690 . . . . . . . . . . . . 13 (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ≠ ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))) → {⟨(2nd𝑇), ((2nd ‘(1st𝑇))‘(2nd𝑇))⟩, ⟨((2nd𝑇) + 1), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
18790, 183, 186syl2anc 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 4669 . . . . . . . . . . . . 13 {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))} = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}
189 f1oeq3 6699 . . . . . . . . . . . . 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 6708 . . . . . . . . . . . . . 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 6723 . . . . . . . . . . . . 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 6715 . . . . . . . . . . . . . . . . 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 6511 . . . . . . . . . . . . . . . 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 6716 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
201 foima 6686 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
20234, 200, 2013syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
203 f1ofo 6716 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
204 foima 6686 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
20558, 203, 2043syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
206202, 205eqtr4d 2781 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ (1...𝑁)))
207128rneqd 5841 . . . . . . . . . . . . . . . . 17 (𝜑 → ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
208 df-ima 5598 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
209 df-ima 5598 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ran ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
210207, 208, 2093eqtr4g 2803 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
211206, 210difeq12d 4058 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
212 dff1o3 6715 . . . . . . . . . . . . . . . . . 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 6511 . . . . . . . . . . . . . . . . 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 4202 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
217 sseqin2 4150 . . . . . . . . . . . . . . . . . . 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 2792 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = {(2nd𝑇), ((2nd𝑇) + 1)})
220219imaeq2d 5963 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
221215, 220eqtr3d 2780 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
222199, 211, 2213eqtrd 2782 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
223219imaeq2d 5963 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}))
224 fnimapr 6845 . . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘(2nd𝑇)), ((2nd ‘(1st𝑇))‘((2nd𝑇) + 1))})
226225, 188eqtrdi 2794 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
227222, 223, 2263eqtr3d 2786 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))})
228227f1oeq3d 6706 . . . . . . . . . . . 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 3996 . . . . . . . . . . . 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 6697 . . . . . . . . . . . . 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 6697 . . . . . . . . . . . . 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 6697 . . . . . . . . . . . . 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 4642 . . . . . . . . . . . 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 1342 . . . . . . . . . 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 14112 . . . . . . . . . 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 8761 . . . . . . . . . . . 12 {(2nd𝑇), ((2nd𝑇) + 1)} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}
240 hashprg 14098 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ∈ V ∧ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ∈ V) → (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ↔ (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2))
24179, 184, 240mp2an 689 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)) ≠ ((2nd ‘(1st𝑇))‘(2nd𝑇)) ↔ (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
24295, 241sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = 2)
243 hashprg 14098 . . . . . . . . . . . . . . . 16 (((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) → ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2))
24473, 74, 243mp2an 689 . . . . . . . . . . . . . . 15 ((2nd𝑇) ≠ ((2nd𝑇) + 1) ↔ (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
24590, 244sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) = 2)
246242, 245eqtr4d 2781 . . . . . . . . . . . . 13 (𝜑 → (♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}))
247 hashen 14049 . . . . . . . . . . . . . 14 (({((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ((♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) ↔ {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)}))
248155, 156, 247mp2an 689 . . . . . . . . . . . . 13 ((♯‘{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}) = (♯‘{(2nd𝑇), ((2nd𝑇) + 1)}) ↔ {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
249246, 248sylib 217 . . . . . . . . . . . 12 (𝜑 → {((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))} ≈ {(2nd𝑇), ((2nd𝑇) + 1)})
250 hashfacen 14154 . . . . . . . . . . . 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 8615 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) = {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
253 mapfi 9103 . . . . . . . . . . . . . . 15 (({(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin ∧ {(2nd𝑇), ((2nd𝑇) + 1)} ∈ Fin) → ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin)
254156, 156, 253mp2an 689 . . . . . . . . . . . . . 14 ({(2nd𝑇), ((2nd𝑇) + 1)} ↑m {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ Fin
255252, 254eqeltrri 2836 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
256 f1of 6709 . . . . . . . . . . . . . 14 (𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} → 𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)})
257256ss2abi 4000 . . . . . . . . . . . . 13 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}
258 ssfi 8944 . . . . . . . . . . . . 13 (({𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin ∧ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ⊆ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}⟶{(2nd𝑇), ((2nd𝑇) + 1)}}) → {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin)
259255, 257, 258mp2an 689 . . . . . . . . . . . 12 {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin
260 hashen 14049 . . . . . . . . . . . 12 (({𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ∈ Fin ∧ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}} ∈ Fin) → ((♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) ↔ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ≈ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}))
261163, 259, 260mp2an 689 . . . . . . . . . . 11 ((♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) ↔ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}} ≈ {𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}})
262251, 261sylibr 233 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}))
263 hashfac 14160 . . . . . . . . . . . 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 6771 . . . . . . . . . . . 12 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = (!‘2))
266 fac2 13981 . . . . . . . . . . . 12 (!‘2) = 2
267265, 266eqtrdi 2794 . . . . . . . . . . 11 (𝜑 → (!‘(♯‘{(2nd𝑇), ((2nd𝑇) + 1)})) = 2)
268264, 267eqtrid 2790 . . . . . . . . . 10 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}}) = 2)
269262, 268eqtrd 2778 . . . . . . . . 9 (𝜑 → (♯‘{𝑓𝑓:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd ‘(1st𝑇))‘((2nd𝑇) + 1)), ((2nd ‘(1st𝑇))‘(2nd𝑇))}}) = 2)
270238, 269breqtrd 5100 . . . . . . . 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 5077 . . . . . . . 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 2961 . . . . 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 6162 . . . . 5 ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((2nd ‘(1st𝑇)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
277128, 276eqtr4di 2796 . . . 4 (𝜑 → ((2nd ‘(1st𝑈)) ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))
278275, 277uneq12d 4098 . . 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 2780 . 2 (𝜑 → (2nd ‘(1st𝑈)) = (((2nd ‘(1st𝑇)) ∘ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}) ∪ ((2nd ‘(1st𝑇)) ∘ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
280 coundi 6145 . 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 2796 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 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  {cab 2715  wne 2943  wral 3064  {crab 3068  Vcvv 3430  csb 3832  cdif 3884  cun 3885  cin 3886  wss 3887  ifcif 4460  {csn 4562  {cpr 4564  {ctp 4566  cop 4568   class class class wbr 5074  cmpt 5157   I cid 5484   × cxp 5583  ccnv 5584  ran crn 5586  cres 5587  cima 5588  ccom 5589  Fun wfun 6421   Fn wfn 6422  wf 6423  1-1wf1 6424  ontowfo 6425  1-1-ontowf1o 6426  cfv 6427  (class class class)co 7268  f cof 7522  1st c1st 7819  2nd c2nd 7820  m cmap 8603  cen 8718  Fincfn 8721  cc 10857  0cc0 10859  1c1 10860   + caddc 10862   < clt 10997  cle 10998  cmin 11193  cn 11961  2c2 12016  3c3 12017  cz 12307  cuz 12570  ...cfz 13227  ..^cfzo 13370  !cfa 13975  chash 14032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5222  ax-nul 5229  ax-pow 5287  ax-pr 5351  ax-un 7579  ax-cnex 10915  ax-resscn 10916  ax-1cn 10917  ax-icn 10918  ax-addcl 10919  ax-addrcl 10920  ax-mulcl 10921  ax-mulrcl 10922  ax-mulcom 10923  ax-addass 10924  ax-mulass 10925  ax-distr 10926  ax-i2m1 10927  ax-1ne0 10928  ax-1rid 10929  ax-rnegex 10930  ax-rrecex 10931  ax-cnre 10932  ax-pre-lttri 10933  ax-pre-lttrn 10934  ax-pre-ltadd 10935  ax-pre-mulgt0 10936
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3432  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6263  df-on 6264  df-lim 6265  df-suc 6266  df-iota 6385  df-fun 6429  df-fn 6430  df-f 6431  df-f1 6432  df-fo 6433  df-f1o 6434  df-fv 6435  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-of 7524  df-om 7704  df-1st 7821  df-2nd 7822  df-frecs 8085  df-wrecs 8116  df-recs 8190  df-rdg 8229  df-1o 8285  df-oadd 8289  df-er 8486  df-map 8605  df-pm 8606  df-en 8722  df-dom 8723  df-sdom 8724  df-fin 8725  df-dju 9647  df-card 9685  df-pnf 10999  df-mnf 11000  df-xr 11001  df-ltxr 11002  df-le 11003  df-sub 11195  df-neg 11196  df-div 11621  df-nn 11962  df-2 12024  df-3 12025  df-n0 12222  df-xnn0 12294  df-z 12308  df-uz 12571  df-fz 13228  df-fzo 13371  df-seq 13710  df-fac 13976  df-bc 14005  df-hash 14033
This theorem is referenced by:  poimirlem22  35785
  Copyright terms: Public domain W3C validator