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 35529

Description: Lemma for poimir 35547, that the face in poimirlem22 35536 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 3596	. . . . . . 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 7793	. . . . 5 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7		xp1st 7793	. . . . 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 7794	. . . . . . . 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 6730	. . . . . . . 8 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6649	. . . . . . . 8 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3587	. . . . . . 7 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 221	. . . . . 6 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		poimirlem15.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
16		elfznn 13141	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
17	15, 16	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
18	17	nnred 11845	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
19	18	ltp1d 11762	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
20	18, 19	ltned 10968	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
21	20	necomd 2996	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇))
22		fvex 6730	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑇) ∈ V
23		ovex 7246	. . . . . . . . . . 11 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
24		f1oprg 6705	. . . . . . . . . . 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 693	. . . . . . . . . 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 587	. . . . . . . . 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 4648	. . . . . . . . . 10 ⊢ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
28		f1oeq3 6651	. . . . . . . . . 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 221	. . . . . . . 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 6698	. . . . . . . 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 4386	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
33		f1oun 6680	. . . . . . . . 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 705	. . . . . . . 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 589	. . . . . . 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 11846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
38		npcan1 11257	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
40	36	nnzd 12281	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
41		peano2zm 12220	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
43		uzid 12453	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
44		peano2uz 12497	. . . . . . . . . . . . . 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 13152	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
49	48, 15	sseldd 3902	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...𝑁))
50	17	peano2nnd 11847	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℕ)
51	42	zred 12282	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
52	36	nnred 11845	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53		elfzle2 13116	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≤ (𝑁 − 1))
54	15, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ (𝑁 − 1))
55	52	ltm1d 11764	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
56	18, 51, 52, 54, 55	lelttrd 10990	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) < 𝑁)
57	17	nnzd 12281	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℤ)
58		zltp1le 12227	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
59	57, 40, 58	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
60	56, 59	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
61		fznn 13180	. . . . . . . . . . . 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 713	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
64		prssi 4734	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
65	49, 63, 64	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
66		undif 4396	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
67	65, 66	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
68		f1oeq23 6652	. . . . . . . 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 587	. . . . . . 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 235	. . . . . 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 6683	. . . . . 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 587	. . . . 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 5325	. . . . . . . 8 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∈ V
74		ovex 7246	. . . . . . . . 9 ⊢ (1...𝑁) ∈ V
75		difexg 5220	. . . . . . . . 9 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V)
76		resiexg 7692	. . . . . . . . 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 7531	. . . . . . 7 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) ∈ V
79	11, 78	coex 7708	. . . . . 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 6649	. . . . . 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 3587	. . . . 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 237	. . . 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 5588	. . . 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 587	. . 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 13208	. . . . 5 ⊢ (1...𝑁) ⊆ (0...𝑁)
86	48, 85	sstrdi 3913	. . . 4 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
87	86, 15	sseldd 3902	. . 3 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
88		opelxpi 5588	. . 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 587	. 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 6717	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
91	90	breq2d 5065	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
92	91	ifbid 4462	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
93	92	csbeq1d 3815	. . . . . . . . 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 6722	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
95		2fveq3 6722	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
96	95	imaeq1d 5928	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
97	96	xpeq1d 5580	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
98	95	imaeq1d 5928	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
99	98	xpeq1d 5580	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
100	97, 99	uneq12d 4078	. . . . . . . . . . 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 7231	. . . . . . . . . 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 3818	. . . . . . . . 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 2777	. . . . . . . 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 5151	. . . . . . 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 2748	. . . . . 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 3605	. . . . 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 500	. . . 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 6115	. . . . . . . . . 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 6662	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
113		incom 4115	. . . . . . . . . . . . . . 15 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
114		elfznn0 13205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ₀)
115	114	nn0red 12151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
116		ltnle 10912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
117	115, 18, 116	syl2anr 600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
118	117	biimpa 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ≤ 𝑦)
119		elfzle2 13116	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ (1...𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
120	118, 119	nsyl 142	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
121		disjsn 4627	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
122	120, 121	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅)
123	115	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ∈ ℝ)
124	18	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ℝ)
125	50	nnred 11845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℝ)
126	125	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
127		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < (2^nd ‘𝑇))
128	19	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
129	123, 124, 126, 127, 128	lttrd 10993	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < ((2^nd ‘𝑇) + 1))
130		ltnle 10912	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ ((2^nd ‘𝑇) + 1) ∈ ℝ) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
131	115, 125, 130	syl2anr 600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
132	131	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
133	129, 132	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦)
134		elfzle2 13116	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) + 1) ∈ (1...𝑦) → ((2^nd ‘𝑇) + 1) ≤ 𝑦)
135	133, 134	nsyl 142	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
136		disjsn 4627	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
137	135, 136	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
138	122, 137	uneq12d 4078	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
139		df-pr 4544	. . . . . . . . . . . . . . . . . 18 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} = ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})
140	139	ineq2i 4124	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
141		indi 4188	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}))
142	140, 141	eqtr2i 2766	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
143		un0 4305	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∪ ∅) = ∅
144	138, 142, 143	3eqtr3g 2801	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
145	113, 144	syl5eq 2790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅)
146		fnimadisj 6510	. . . . . . . . . . . . . 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 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
148	39	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
149		elfzuz3 13109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑦))
150		peano2uz 12497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
152	151	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
153	148, 152	eqeltrrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘𝑦))
154		fzss2 13152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑦) → (1...𝑦) ⊆ (1...𝑁))
155		reldisj 4366	. . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
158	144, 157	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
159		resiima 5944	. . . . . . . . . . . . . 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 4078	. . . . . . . . . . . 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 6014	. . . . . . . . . . . 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 4067	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
164		un0 4305	. . . . . . . . . . . . 13 ⊢ ((1...𝑦) ∪ ∅) = (1...𝑦)
165	163, 164	eqtr2i 2766	. . . . . . . . . . . 12 ⊢ (1...𝑦) = (∅ ∪ (1...𝑦))
166	161, 162, 165	3eqtr4g 2803	. . . . . . . . . . 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 5929	. . . . . . . . . 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	syl5eq 2790	. . . . . . . . 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 5580	. . . . . . . 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 6115	. . . . . . . . . 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 6014	. . . . . . . . . . . . 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 5940	. . . . . . . . . . . . . . . . 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 6508	. . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . 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 13112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
178		zltp1le 12227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℤ ∧ (2^nd ‘𝑇) ∈ ℤ) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
179	177, 57, 178	syl2anr 600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
180	179	biimpa 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ (2^nd ‘𝑇))
181	18, 52, 56	ltled 10980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ 𝑁)
182	181	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑁)
183	57	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ ℤ)
184		nn0p1nn 12129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ ℕ)
185	114, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
186	185	nnzd 12281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
187	186	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
188	40	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
189		elfz 13101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
190	183, 187, 188, 189	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
191	190	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
192	180, 182, 191	mpbir2and 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁))
193		1red 10834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 1 ∈ ℝ)
194		ltle 10921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
195	115, 18, 194	syl2anr 600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
196	195	imp 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ≤ (2^nd ‘𝑇))
197	123, 124, 193, 196	leadd1dd 11446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1))
198	60	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
199	57	peano2zd 12285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℤ)
200	199	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ ℤ)
201		elfz 13101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
202	200, 187, 188, 201	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
203	202	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
204	197, 198, 203	mpbir2and 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
205		prssi 4734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
206	192, 204, 205	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207		imass2 5970	. . . . . . . . . . . . . . . . . 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 3940	. . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . 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 6668	. . . . . . . . . . . . . . . . . 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 6636	. . . . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
215	214	ad2antrr 726	. . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
217		undif 4396	. . . . . . . . . . . . . . . . 17 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
218	206, 217	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
219	218	imaeq2d 5929	. . . . . . . . . . . . . . 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 6506	. . . . . . . . . . . . . . . . . . 19 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
221		disjdifr 4387	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅
222		fnimadisj 6510	. . . . . . . . . . . . . . . . . . 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 692	. . . . . . . . . . . . . . . . . 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 12477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
226	185, 225	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ_≥‘1))
227		fzss1 13151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
228	226, 227	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
229	228	ssdifd 4055	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
230		resiima 5944	. . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . 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 4078	. . . . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . . . 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 4067	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
236		un0 4305	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
237	235, 236	eqtr2i 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
238	233, 234, 237	3eqtr4g 2803	. . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
240	216, 239	uneq12d 4078	. . . . . . . . . . . . 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	syl5eq 2790	. . . . . . . . . . . 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 2777	. . . . . . . . . . 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 5929	. . . . . . . . . 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	syl5eq 2790	. . . . . . . . 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 5580	. . . . . . . 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 4078	. . . . . . 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 7229	. . . . . 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 4445	. . . . . . . . 9 ⊢ (𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
249	248	csbeq1d 3815	. . . . . . . 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 3412	. . . . . . . . 9 ⊢ 𝑦 ∈ V
251		oveq2 7221	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
252	251	imaeq2d 5929	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 7220	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
255	254	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
256	255	imaeq2d 5929	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 4078	. . . . . . . . . 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 7229	. . . . . . . . 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 3847	. . . . . . . 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 2794	. . . . . . 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 485	. . . . . 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 3815	. . . . . . . 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 5929	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
265	264	xpeq1d 5580	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
266	255	imaeq2d 5929	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
267	266	xpeq1d 5580	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
268	265, 267	uneq12d 4078	. . . . . . . . . 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 7229	. . . . . . . . 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 3847	. . . . . . . 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 2794	. . . . . . 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 485	. . . . . 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 2787	. . . . 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 10911	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
275	18, 115, 274	syl2an 599	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
276	275	biimpar 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑦)
277		imaco 6115	. . . . . . . . . . 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 6014	. . . . . . . . . . . . . 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 5940	. . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℕ)
283	18	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℝ)
284	115	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
285	185	nnred 11845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
286	285	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
287		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
288	115	lep1d 11763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
289	288	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
290	283, 284, 286, 287, 289	letrd 10989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ (𝑦 + 1))
291		fznn 13180	. . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
294	282, 290, 293	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ (1...(𝑦 + 1)))
295	50	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℕ)
296		1red 10834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 1 ∈ ℝ)
297	283, 284, 296, 287	leadd1dd 11446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))
298		fznn 13180	. . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
301	295, 297, 300	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)))
302		prssi 4734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
303	294, 301, 302	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
304		imass2 5970	. . . . . . . . . . . . . . . . . . 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 3940	. . . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
310		undif 4396	. . . . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...(𝑦 + 1)))
312	311	imaeq2d 5929	. . . . . . . . . . . . . . . 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 12466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
315	149, 314	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
316	315	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
317	148, 316	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑦 + 1)))
318		fzss2 13152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
319	317, 318	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
320	319	ssdifd 4055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
321	320	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
322		resiima 5944	. . . . . . . . . . . . . . . . . . 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 4078	. . . . . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . . . . 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 4067	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
327		un0 4305	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
328	326, 327	eqtr2i 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
329	324, 325, 328	3eqtr4g 2803	. . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . . 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 4078	. . . . . . . . . . . . . 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	syl5eq 2790	. . . . . . . . . . . . 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 2777	. . . . . . . . . . . 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 5929	. . . . . . . . . . 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	syl5eq 2790	. . . . . . . . . 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 5580	. . . . . . . . 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 6115	. . . . . . . . . . 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 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
339		incom 4115	. . . . . . . . . . . . . . . 16 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
340	125	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
341	185	peano2nnd 11847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
342	341	nnred 11845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
343	342	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
344	19	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
345	115	ltp1d 11762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
346	345	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
347	283, 284, 286, 287, 346	lelttrd 10990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < (𝑦 + 1))
348	283, 286, 296, 347	ltadd1dd 11443	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1))
349	283, 340, 343, 344, 348	lttrd 10993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((𝑦 + 1) + 1))
350		ltnle 10912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
351	18, 342, 350	syl2an 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
352	351	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
353	349, 352	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
354		elfzle1 13115	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
355	353, 354	nsyl 142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
356		disjsn 4627	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
357	355, 356	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅)
358		ltnle 10912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
359	125, 342, 358	syl2an 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
360	359	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
361	348, 360	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
362		elfzle1 13115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
363	361, 362	nsyl 142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
364		disjsn 4627	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
365	363, 364	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
366	357, 365	uneq12d 4078	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
367	139	ineq2i 4124	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
368		indi 4188	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}))
369	367, 368	eqtr2i 2766	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
370	366, 369, 143	3eqtr3g 2801	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
371	339, 370	syl5eq 2790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
372		fnimadisj 6510	. . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . 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 13151	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 + 1) + 1) ∈ (ℤ_≥‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
376		reldisj 4366	. . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
379	370, 378	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
380		resiima 5944	. . . . . . . . . . . . . . 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 4078	. . . . . . . . . . . . 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 6014	. . . . . . . . . . . . 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 4067	. . . . . . . . . . . . . 14 ⊢ (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
385		un0 4305	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
386	384, 385	eqtr2i 2766	. . . . . . . . . . . . 13 ⊢ (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
387	382, 383, 386	3eqtr4g 2803	. . . . . . . . . . . 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 5929	. . . . . . . . . . 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	syl5eq 2790	. . . . . . . . . 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 5580	. . . . . . . . 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 4078	. . . . . . . 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 594	. . . . . . 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 7229	. . . . . 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 4448	. . . . . . . . 9 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
395	394	csbeq1d 3815	. . . . . . . 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 7246	. . . . . . . . 9 ⊢ (𝑦 + 1) ∈ V
397		oveq2 7221	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
398	397	imaeq2d 5929	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 7220	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
401	400	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
402	401	imaeq2d 5929	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 4078	. . . . . . . . . 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 7229	. . . . . . . . 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 3847	. . . . . . . 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 2794	. . . . . . 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 485	. . . . . 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 3815	. . . . . . . 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 5929	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
411	410	xpeq1d 5580	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}))
412	401	imaeq2d 5929	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
413	412	xpeq1d 5580	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
414	411, 413	uneq12d 4078	. . . . . . . . . 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 7229	. . . . . . . . 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 3847	. . . . . . . 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 2794	. . . . . . 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 485	. . . . . 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 2787	. . . . 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 813	. . . 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 5150	. . 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 2780	. 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 5348	. . . . . . 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 7771	. . . . . 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 7772	. . . . . 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 5057	. . . . . . . . 9 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
427	426	ifbid 4462	. . . . . . . 8 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
428	427	csbeq1d 3815	. . . . . . 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 6730	. . . . . . . . . 10 ⊢ (1^st ‘(1^st ‘𝑇)) ∈ V
430	429, 79	op1std 7771	. . . . . . . . 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 7772	. . . . . . . . 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 5924	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 5924	. . . . . . . . . . . 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 5580	. . . . . . . . . . 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 4078	. . . . . . . . . 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 7232	. . . . . . . . 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 587	. . . . . . . 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 3818	. . . . . . 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 2800	. . . . . 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 587	. . . . 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 5151	. . . 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 2748	. . 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 3605	. 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 586	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 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 {cab 2714 ≠ wne 2940 {crab 3065 Vcvv 3408 ⦋csb 3811 ∖ cdif 3863 ∪ cun 3864 ∩ cin 3865 ⊆ wss 3866 ∅c0 4237 ifcif 4439 {csn 4541 {cpr 4543 ⟨cop 4547 class class class wbr 5053 ↦ cmpt 5135 I cid 5454 × cxp 5549 ran crn 5552 ↾ cres 5553 “ cima 5554 ∘ ccom 5555 Fn wfn 6375 ⟶wf 6376 –onto→wfo 6378 –1-1-onto→wf1o 6379 ‘cfv 6380 (class class class)co 7213 ∘_f cof 7467 1^st c1st 7759 2^nd c2nd 7760 ↑_m cmap 8508 ℂcc 10727 ℝcr 10728 0cc0 10729 1c1 10730 + caddc 10732 < clt 10867 ≤ cle 10868 − cmin 11062 ℕcn 11830 ℕ₀cn0 12090 ℤcz 12176 ℤ_≥cuz 12438 ...cfz 13095 ..^cfzo 13238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-er 8391 df-en 8627 df-dom 8628 df-sdom 8629 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-nn 11831 df-n0 12091 df-z 12177 df-uz 12439 df-fz 13096

This theorem is referenced by: poimirlem22 35536

W3C validator