poimirlem15 - Mathbox for Brendan Leahy

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

Theorem poimirlem15 36093

Description: Lemma for poimir 36111, that the face in poimirlem22 36100 is a face. (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(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1	⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
poimirlem22.2	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem15.3	⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))

**Assertion**
Ref	Expression
poimirlem15	⊢ (𝜑 → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆)

Distinct variable groups: 𝑓,𝑗,𝑡,𝑦 𝜑,𝑗,𝑦 𝑗,𝐹,𝑦 𝑗,𝑁,𝑦 𝑇,𝑗,𝑦 𝜑,𝑡 𝑓,𝐾,𝑗,𝑡 𝑓,𝑁,𝑡 𝑇,𝑓 𝑓,𝐹,𝑡 𝑡,𝑇 𝑆,𝑗,𝑡,𝑦 Allowed substitution hints: 𝜑(𝑓) 𝑆(𝑓) 𝐾(𝑦)

**Proof of Theorem poimirlem15**
Step	Hyp	Ref	Expression
1		poimirlem22.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
2		elrabi 3639	. . . . . . 7 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3		poimirlem22.s	. . . . . . 7 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4	2, 3	eleq2s 2856	. . . . . 6 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5	1, 4	syl 17	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6		xp1st 7953	. . . . 5 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7		xp1st 7953	. . . . 5 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
8	5, 6, 7	3syl 18	. . . 4 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
9		xp2nd 7954	. . . . . . . 8 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10	5, 6, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11		fvex 6855	. . . . . . . 8 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6772	. . . . . . . 8 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3630	. . . . . . 7 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 217	. . . . . 6 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		poimirlem15.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
16		elfznn 13470	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
17	15, 16	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
18	17	nnred 12168	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
19	18	ltp1d 12085	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
20	18, 19	ltned 11291	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
21	20	necomd 2999	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇))
22		fvex 6855	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑇) ∈ V
23		ovex 7390	. . . . . . . . . . 11 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
24		f1oprg 6829	. . . . . . . . . . 11 ⊢ ((((2^nd ‘𝑇) ∈ V ∧ ((2^nd ‘𝑇) + 1) ∈ V) ∧ (((2^nd ‘𝑇) + 1) ∈ V ∧ (2^nd ‘𝑇) ∈ V)) → (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)}))
25	22, 23, 23, 22, 24	mp4an 691	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
26	20, 21, 25	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
27		prcom 4693	. . . . . . . . . 10 ⊢ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
28		f1oeq3 6774	. . . . . . . . . 10 ⊢ ({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
29	27, 28	ax-mp 5	. . . . . . . . 9 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
30	26, 29	sylib 217	. . . . . . . 8 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
31		f1oi 6822	. . . . . . . 8 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
32		disjdif 4431	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
33		f1oun 6803	. . . . . . . . 9 ⊢ ((({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ∧ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
34	32, 32, 33	mpanr12 703	. . . . . . . 8 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
35	30, 31, 34	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
36		poimir.0	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
37	36	nncnd 12169	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
38		npcan1 11580	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
40	36	nnzd 12526	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
41		peano2zm 12546	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
43		uzid 12778	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
44		peano2uz 12826	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
45	42, 43, 44	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
46	39, 45	eqeltrrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
47		fzss2 13481	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
49	48, 15	sseldd 3945	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...𝑁))
50	17	peano2nnd 12170	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℕ)
51	42	zred 12607	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
52	36	nnred 12168	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53		elfzle2 13445	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≤ (𝑁 − 1))
54	15, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ (𝑁 − 1))
55	52	ltm1d 12087	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
56	18, 51, 52, 54, 55	lelttrd 11313	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) < 𝑁)
57	17	nnzd 12526	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℤ)
58		zltp1le 12553	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
59	57, 40, 58	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
60	56, 59	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
61		fznn 13509	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
62	40, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
63	50, 60, 62	mpbir2and 711	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
64		prssi 4781	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
65	49, 63, 64	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
66		undif 4441	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
67	65, 66	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
68		f1oeq23 6775	. . . . . . . 8 ⊢ ((({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁) ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ↔ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
69	67, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ↔ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
70	35, 69	mpbid 231	. . . . . 6 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁))
71		f1oco 6807	. . . . . 6 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
72	14, 70, 71	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
73		prex 5389	. . . . . . . 8 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∈ V
74		ovex 7390	. . . . . . . . 9 ⊢ (1...𝑁) ∈ V
75		difexg 5284	. . . . . . . . 9 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V)
76		resiexg 7851	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V → ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ∈ V)
77	74, 75, 76	mp2b 10	. . . . . . . 8 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ∈ V
78	73, 77	unex 7680	. . . . . . 7 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) ∈ V
79	11, 78	coex 7867	. . . . . 6 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ V
80		f1oeq1 6772	. . . . . 6 ⊢ (𝑓 = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁)))
81	79, 80	elab 3630	. . . . 5 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
82	72, 81	sylibr 233	. . . 4 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
83		opelxpi 5670	. . . 4 ⊢ (((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) ∧ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
84	8, 82, 83	syl2anc 584	. . 3 ⊢ (𝜑 → ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
85		fz1ssfz0 13537	. . . . 5 ⊢ (1...𝑁) ⊆ (0...𝑁)
86	48, 85	sstrdi 3956	. . . 4 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
87	86, 15	sseldd 3945	. . 3 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
88		opelxpi 5670	. . 3 ⊢ ((⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (2^nd ‘𝑇) ∈ (0...𝑁)) → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
89	84, 87, 88	syl2anc 584	. 2 ⊢ (𝜑 → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
90		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
91	90	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
92	91	ifbid 4509	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
93	92	csbeq1d 3859	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
94		2fveq3 6847	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
95		2fveq3 6847	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
96	95	imaeq1d 6012	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
97	96	xpeq1d 5662	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
98	95	imaeq1d 6012	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
99	98	xpeq1d 5662	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
100	97, 99	uneq12d 4124	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
101	94, 100	oveq12d 7375	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
102	101	csbeq2dv 3862	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
103	93, 102	eqtrd 2776	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
104	103	mpteq2dv 5207	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
105	104	eqeq2d 2747	. . . . . 6 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
106	105, 3	elrab2 3648	. . . . 5 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
107	106	simprbi 497	. . . 4 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
108	1, 107	syl 17	. . 3 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
109		imaco 6203	. . . . . . . . . 10 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) = ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦)))
110		f1ofn 6785	. . . . . . . . . . . . . . . 16 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
111	26, 110	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
112	111	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
113		incom 4161	. . . . . . . . . . . . . . 15 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
114		elfznn0 13534	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ₀)
115	114	nn0red 12474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
116		ltnle 11234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
117	115, 18, 116	syl2anr 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
118	117	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ≤ 𝑦)
119		elfzle2 13445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ (1...𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
120	118, 119	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
121		disjsn 4672	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
122	120, 121	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅)
123	115	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ∈ ℝ)
124	18	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ℝ)
125	50	nnred 12168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℝ)
126	125	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
127		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < (2^nd ‘𝑇))
128	19	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
129	123, 124, 126, 127, 128	lttrd 11316	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < ((2^nd ‘𝑇) + 1))
130		ltnle 11234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ ((2^nd ‘𝑇) + 1) ∈ ℝ) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
131	115, 125, 130	syl2anr 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
132	131	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
133	129, 132	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦)
134		elfzle2 13445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) + 1) ∈ (1...𝑦) → ((2^nd ‘𝑇) + 1) ≤ 𝑦)
135	133, 134	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
136		disjsn 4672	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
137	135, 136	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
138	122, 137	uneq12d 4124	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
139		df-pr 4589	. . . . . . . . . . . . . . . . . 18 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} = ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})
140	139	ineq2i 4169	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
141		indi 4233	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}))
142	140, 141	eqtr2i 2765	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
143		un0 4350	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∪ ∅) = ∅
144	138, 142, 143	3eqtr3g 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
145	113, 144	eqtrid 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅)
146		fnimadisj 6633	. . . . . . . . . . . . . 14 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
147	112, 145, 146	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
148	39	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
149		elfzuz3 13438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑦))
150		peano2uz 12826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
152	151	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
153	148, 152	eqeltrrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘𝑦))
154		fzss2 13481	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑦) → (1...𝑦) ⊆ (1...𝑁))
155		reldisj 4411	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ⊆ (1...𝑁) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
156	153, 154, 155	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
157	156	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
158	144, 157	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
159		resiima 6028	. . . . . . . . . . . . . 14 ⊢ ((1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
160	158, 159	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
161	147, 160	uneq12d 4124	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦))) = (∅ ∪ (1...𝑦)))
162		imaundir 6103	. . . . . . . . . . . 12 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦)) = (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)))
163		uncom 4113	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
164		un0 4350	. . . . . . . . . . . . 13 ⊢ ((1...𝑦) ∪ ∅) = (1...𝑦)
165	163, 164	eqtr2i 2765	. . . . . . . . . . . 12 ⊢ (1...𝑦) = (∅ ∪ (1...𝑦))
166	161, 162, 165	3eqtr4g 2801	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦)) = (1...𝑦))
167	166	imaeq2d 6013	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
168	109, 167	eqtrid 2788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
169	168	xpeq1d 5662	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
170		imaco 6203	. . . . . . . . . 10 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)))
171		imaundir 6103	. . . . . . . . . . . . 13 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)))
172		imassrn 6024	. . . . . . . . . . . . . . . . 17 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ⊆ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}
173	172	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ⊆ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
174		fnima 6631	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
175	26, 110, 174	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
176	175	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
177		elfzelz 13441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
178		zltp1le 12553	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℤ ∧ (2^nd ‘𝑇) ∈ ℤ) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
179	177, 57, 178	syl2anr 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
180	179	biimpa 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ (2^nd ‘𝑇))
181	18, 52, 56	ltled 11303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ 𝑁)
182	181	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑁)
183	57	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ ℤ)
184		nn0p1nn 12452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ ℕ)
185	114, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
186	185	nnzd 12526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
187	186	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
188	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
189		elfz 13430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
190	183, 187, 188, 189	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
191	190	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
192	180, 182, 191	mpbir2and 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁))
193		1red 11156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 1 ∈ ℝ)
194		ltle 11243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
195	115, 18, 194	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
196	195	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ≤ (2^nd ‘𝑇))
197	123, 124, 193, 196	leadd1dd 11769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1))
198	60	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
199	57	peano2zd 12610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℤ)
200	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ ℤ)
201		elfz 13430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
202	200, 187, 188, 201	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
203	202	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
204	197, 198, 203	mpbir2and 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
205		prssi 4781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
206	192, 204, 205	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207		imass2 6054	. . . . . . . . . . . . . . . . . 18 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
208	206, 207	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
209	176, 208	eqsstrrd 3983	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
210	173, 209	eqssd 3961	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
211		f1ofo 6791	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
212		forn 6759	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
213	26, 211, 212	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
214	213, 27	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
215	214	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
216	210, 215	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
217		undif 4441	. . . . . . . . . . . . . . . . 17 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
218	206, 217	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
219	218	imaeq2d 6013	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)))
220		fnresi 6630	. . . . . . . . . . . . . . . . . . 19 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
221		disjdifr 4432	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅
222		fnimadisj 6633	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
223	220, 221, 222	mp2an 690	. . . . . . . . . . . . . . . . . 18 ⊢ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅
224	223	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
225		nnuz 12806	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
226	185, 225	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ_≥‘1))
227		fzss1 13480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
228	226, 227	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
229	228	ssdifd 4100	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
230		resiima 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
231	229, 230	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
232	231	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
233	224, 232	uneq12d 4124	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
234		imaundi 6102	. . . . . . . . . . . . . . . 16 ⊢ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
235		uncom 4113	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
236		un0 4350	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
237	235, 236	eqtr2i 2765	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
238	233, 234, 237	3eqtr4g 2801	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
239	219, 238	eqtr3d 2778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
240	216, 239	uneq12d 4124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
241	171, 240	eqtrid 2788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
242	241, 218	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ((𝑦 + 1)...𝑁))
243	242	imaeq2d 6013	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
244	170, 243	eqtrid 2788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
245	244	xpeq1d 5662	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
246	169, 245	uneq12d 4124	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
247	246	oveq2d 7373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
248		iftrue 4492	. . . . . . . . 9 ⊢ (𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
249	248	csbeq1d 3859	. . . . . . . 8 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
250		vex 3449	. . . . . . . . 9 ⊢ 𝑦 ∈ V
251		oveq2 7365	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
252	251	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)))
253	252	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}))
254		oveq1 7364	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
255	254	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
256	255	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)))
257	256	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))
258	253, 257	uneq12d 4124	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})))
259	258	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
260	250, 259	csbie 3891	. . . . . . . 8 ⊢ ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})))
261	249, 260	eqtrdi 2792	. . . . . . 7 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
262	261	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
263	248	csbeq1d 3859	. . . . . . . 8 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
264	251	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
265	264	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
266	255	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
267	266	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
268	265, 267	uneq12d 4124	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
269	268	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
270	250, 269	csbie 3891	. . . . . . . 8 ⊢ ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
271	263, 270	eqtrdi 2792	. . . . . . 7 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
272	271	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
273	247, 262, 272	3eqtr4d 2786	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
274		lenlt 11233	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
275	18, 115, 274	syl2an 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
276	275	biimpar 478	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑦)
277		imaco 6203	. . . . . . . . . . 11 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1))))
278		imaundir 6103	. . . . . . . . . . . . . 14 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1))) = (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...(𝑦 + 1))))
279		imassrn 6024	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) ⊆ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}
280	279	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) ⊆ ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
281	175	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
282	17	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℕ)
283	18	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℝ)
284	115	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
285	185	nnred 12168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
286	285	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
287		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
288	115	lep1d 12086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
289	288	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
290	283, 284, 286, 287, 289	letrd 11312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ (𝑦 + 1))
291		fznn 13509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
292	186, 291	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
293	292	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
294	282, 290, 293	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ (1...(𝑦 + 1)))
295	50	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℕ)
296		1red 11156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 1 ∈ ℝ)
297	283, 284, 296, 287	leadd1dd 11769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))
298		fznn 13509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
299	186, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
300	299	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
301	295, 297, 300	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)))
302		prssi 4781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
303	294, 301, 302	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
304		imass2 6054	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))))
305	303, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))))
306	281, 305	eqsstrrd 3983	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))))
307	280, 306	eqssd 3961	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
308	214	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
309	307, 308	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
310		undif 4441	. . . . . . . . . . . . . . . . . 18 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...(𝑦 + 1)))
311	303, 310	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...(𝑦 + 1)))
312	311	imaeq2d 6013	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...(𝑦 + 1))))
313	223	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
314		eluzp1p1 12791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
315	149, 314	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
316	315	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
317	148, 316	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑦 + 1)))
318		fzss2 13481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
319	317, 318	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
320	319	ssdifd 4100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
321	320	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
322		resiima 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
323	321, 322	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
324	313, 323	uneq12d 4124	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
325		imaundi 6102	. . . . . . . . . . . . . . . . 17 ⊢ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
326		uncom 4113	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
327		un0 4350	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
328	326, 327	eqtr2i 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
329	324, 325, 328	3eqtr4g 2801	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
330	312, 329	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...(𝑦 + 1))) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
331	309, 330	uneq12d 4124	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...(𝑦 + 1)))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
332	278, 331	eqtrid 2788	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
333	332, 311	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1))) = (1...(𝑦 + 1)))
334	333	imaeq2d 6013	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1)))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
335	277, 334	eqtrid 2788	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
336	335	xpeq1d 5662	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}))
337		imaco 6203	. . . . . . . . . . 11 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)))
338	111	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
339		incom 4161	. . . . . . . . . . . . . . . 16 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
340	125	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
341	185	peano2nnd 12170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
342	341	nnred 12168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
343	342	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
344	19	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
345	115	ltp1d 12085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
346	345	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
347	283, 284, 286, 287, 346	lelttrd 11313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < (𝑦 + 1))
348	283, 286, 296, 347	ltadd1dd 11766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1))
349	283, 340, 343, 344, 348	lttrd 11316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((𝑦 + 1) + 1))
350		ltnle 11234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
351	18, 342, 350	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
352	351	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
353	349, 352	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
354		elfzle1 13444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
355	353, 354	nsyl 140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
356		disjsn 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
357	355, 356	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅)
358		ltnle 11234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
359	125, 342, 358	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
360	359	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
361	348, 360	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
362		elfzle1 13444	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
363	361, 362	nsyl 140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
364		disjsn 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
365	363, 364	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
366	357, 365	uneq12d 4124	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
367	139	ineq2i 4169	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
368		indi 4233	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}))
369	367, 368	eqtr2i 2765	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
370	366, 369, 143	3eqtr3g 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
371	339, 370	eqtrid 2788	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
372		fnimadisj 6633	. . . . . . . . . . . . . . 15 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
373	338, 371, 372	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
374	341, 225	eleqtrdi 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ_≥‘1))
375		fzss1 13480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 + 1) + 1) ∈ (ℤ_≥‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
376		reldisj 4411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
377	374, 375, 376	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
378	377	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
379	370, 378	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
380		resiima 6028	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
381	379, 380	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
382	373, 381	uneq12d 4124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁))) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁)))
383		imaundir 6103	. . . . . . . . . . . . 13 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)))
384		uncom 4113	. . . . . . . . . . . . . 14 ⊢ (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
385		un0 4350	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
386	384, 385	eqtr2i 2765	. . . . . . . . . . . . 13 ⊢ (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
387	382, 383, 386	3eqtr4g 2801	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
388	387	imaeq2d 6013	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
389	337, 388	eqtrid 2788	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
390	389	xpeq1d 5662	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
391	336, 390	uneq12d 4124	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
392	276, 391	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
393	392	oveq2d 7373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
394		iffalse 4495	. . . . . . . . 9 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
395	394	csbeq1d 3859	. . . . . . . 8 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
396		ovex 7390	. . . . . . . . 9 ⊢ (𝑦 + 1) ∈ V
397		oveq2 7365	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
398	397	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))))
399	398	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}))
400		oveq1 7364	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
401	400	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
402	401	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)))
403	402	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
404	399, 403	uneq12d 4124	. . . . . . . . . 10 ⊢ (𝑗 = (𝑦 + 1) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
405	404	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑗 = (𝑦 + 1) → ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
406	396, 405	csbie 3891	. . . . . . . 8 ⊢ ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
407	395, 406	eqtrdi 2792	. . . . . . 7 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
408	407	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
409	394	csbeq1d 3859	. . . . . . . 8 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
410	397	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
411	410	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}))
412	401	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
413	412	xpeq1d 5662	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
414	411, 413	uneq12d 4124	. . . . . . . . . 10 ⊢ (𝑗 = (𝑦 + 1) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
415	414	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑗 = (𝑦 + 1) → ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
416	396, 415	csbie 3891	. . . . . . . 8 ⊢ ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
417	409, 416	eqtrdi 2792	. . . . . . 7 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
418	417	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
419	393, 408, 418	3eqtr4d 2786	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
420	273, 419	pm2.61dan 811	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
421	420	mpteq2dva 5205	. . 3 ⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
422	108, 421	eqtr4d 2779	. 2 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))))
423		opex 5421	. . . . . . 7 ⊢ ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ V
424	423, 22	op1std 7931	. . . . . 6 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → (1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩)
425	423, 22	op2ndd 7932	. . . . . 6 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → (2^nd ‘𝑡) = (2^nd ‘𝑇))
426		breq2 5109	. . . . . . . . 9 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
427	426	ifbid 4509	. . . . . . . 8 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
428	427	csbeq1d 3859	. . . . . . 7 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
429		fvex 6855	. . . . . . . . . 10 ⊢ (1^st ‘(1^st ‘𝑇)) ∈ V
430	429, 79	op1std 7931	. . . . . . . . 9 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
431	429, 79	op2ndd 7932	. . . . . . . . 9 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
432		id 22	. . . . . . . . . 10 ⊢ ((1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)) → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
433		imaeq1 6008	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)))
434	433	xpeq1d 5662	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}))
435		imaeq1 6008	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)))
436	435	xpeq1d 5662	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))
437	434, 436	uneq12d 4124	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))
438	432, 437	oveqan12d 7376	. . . . . . . . 9 ⊢ (((1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
439	430, 431, 438	syl2anc 584	. . . . . . . 8 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
440	439	csbeq2dv 3862	. . . . . . 7 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
441	428, 440	sylan9eqr 2798	. . . . . 6 ⊢ (((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∧ (2^nd ‘𝑡) = (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
442	424, 425, 441	syl2anc 584	. . . . 5 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
443	442	mpteq2dv 5207	. . . 4 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))))
444	443	eqeq2d 2747	. . 3 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
445	444, 3	elrab2 3648	. 2 ⊢ (⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆 ↔ (⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
446	89, 422, 445	sylanbrc 583	1 ⊢ (𝜑 → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2713 ≠ wne 2943 {crab 3407 Vcvv 3445 ⦋csb 3855 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 {csn 4586 {cpr 4588 ⟨cop 4592 class class class wbr 5105 ↦ cmpt 5188 I cid 5530 × cxp 5631 ran crn 5634 ↾ cres 5635 “ cima 5636 ∘ ccom 5637 Fn wfn 6491 ⟶wf 6492 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 1^st c1st 7919 2^nd c2nd 7920 ↑_m cmap 8765 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 ≤ cle 11190 − cmin 11385 ℕcn 12153 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ...cfz 13424 ..^cfzo 13567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-n0 12414 df-z 12500 df-uz 12764 df-fz 13425

This theorem is referenced by: poimirlem22 36100

W3C validator