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 38209

Description: Lemma for poimir 38227, that the face in poimirlem22 38216 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 3653	. . . . . . 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 2887	. . . . . 6 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5	1, 4	syl 18	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6		xp1st 8018	. . . . 5 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7		xp1st 8018	. . . . 5 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
8	5, 6, 7	3syl 19	. . . 4 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
9		xp2nd 8019	. . . . . . . 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 19	. . . . . . 7 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11		fvex 6895	. . . . . . . 8 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6809	. . . . . . . 8 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3645	. . . . . . 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 13581	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
17	15, 16	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
18	17	nnred 12248	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
19	18	ltp1d 12145	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
20	18, 19	ltned 11346	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
21	20	necomd 3019	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇))
22		fvex 6895	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑇) ∈ V
23		ovex 7444	. . . . . . . . . . 11 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
24		f1oprg 6868	. . . . . . . . . . 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 705	. . . . . . . . . 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 595	. . . . . . . . 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 4701	. . . . . . . . . 10 ⊢ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
28		f1oeq3 6811	. . . . . . . . . 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 6860	. . . . . . . 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 4436	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
33		f1oun 6841	. . . . . . . . 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 717	. . . . . . . 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 597	. . . . . . 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 12249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
38		npcan1 11639	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
39	37, 38	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
40	36	nnzd 12617	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
41		peano2zm 12637	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
42	40, 41	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
43		uzid 12877	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
44		peano2uz 12925	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
45	42, 43, 44	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
46	39, 45	eqeltrrd 2870	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
47		fzss2 13592	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
48	46, 47	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
49	48, 15	sseldd 3944	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...𝑁))
50	17	peano2nnd 12250	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℕ)
51	42	zred 12700	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
52	36	nnred 12248	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53		elfzle2 13556	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≤ (𝑁 − 1))
54	15, 53	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ (𝑁 − 1))
55	52	ltm1d 12147	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
56	18, 51, 52, 54, 55	lelttrd 11368	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) < 𝑁)
57	17	nnzd 12617	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℤ)
58		zltp1le 12644	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
59	57, 40, 58	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
60	56, 59	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
61		fznn 13620	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
62	40, 61	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
63	50, 60, 62	mpbir2and 725	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
64		prssi 4789	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
65	49, 63, 64	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
66		undif 4446	. . . . . . . . 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 6812	. . . . . . . 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 595	. . . . . . 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 6845	. . . . . 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 595	. . . . 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 5410	. . . . . . . 8 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∈ V
74		ovex 7444	. . . . . . . . 9 ⊢ (1...𝑁) ∈ V
75		difexg 5300	. . . . . . . . 9 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V)
76		resiexg 7909	. . . . . . . . 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 7743	. . . . . . 7 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) ∈ V
79	11, 78	coex 7927	. . . . . 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 6809	. . . . . 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 3645	. . . . 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 5699	. . . 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 595	. . 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 13651	. . . . 5 ⊢ (1...𝑁) ⊆ (0...𝑁)
86	48, 85	sstrdi 3955	. . . 4 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
87	86, 15	sseldd 3944	. . 3 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
88		opelxpi 5699	. . 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 595	. 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 6882	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
91	90	breq2d 5123	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
92	91	ifbid 4514	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
93	92	csbeq1d 3863	. . . . . . . . 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 6887	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
95		2fveq3 6887	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
96	95	imaeq1d 6062	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
97	96	xpeq1d 5691	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
98	95	imaeq1d 6062	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
99	98	xpeq1d 5691	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
100	97, 99	uneq12d 4129	. . . . . . . . . . 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 7429	. . . . . . . . . 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 3866	. . . . . . . . 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 2804	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
104	103	mpteq2dv 5207	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
105	104	eqeq2d 2780	. . . . . 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 3661	. . . . 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 502	. . . 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 18	. . 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 6253	. . . . . . . . . 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 6822	. . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
112	111	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
113		incom 4168	. . . . . . . . . . . . . . 15 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
114		elfznn0 13648	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ₀)
115	114	nn0red 12566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
116		ltnle 11289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
117	115, 18, 116	syl2anr 608	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
118	117	biimpa 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ≤ 𝑦)
119		elfzle2 13556	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ (1...𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
120	118, 119	nsyl 141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
121		disjsn 4680	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
122	120, 121	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅)
123	115	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ∈ ℝ)
124	18	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ℝ)
125	50	nnred 12248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℝ)
126	125	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
127		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < (2^nd ‘𝑇))
128	19	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
129	123, 124, 126, 127, 128	lttrd 11371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < ((2^nd ‘𝑇) + 1))
130		ltnle 11289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ ((2^nd ‘𝑇) + 1) ∈ ℝ) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
131	115, 125, 130	syl2anr 608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
132	131	adantr 485	. . . . . . . . . . . . . . . . . . . 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 13556	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) + 1) ∈ (1...𝑦) → ((2^nd ‘𝑇) + 1) ≤ 𝑦)
135	133, 134	nsyl 141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
136		disjsn 4680	. . . . . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
139		df-pr 4595	. . . . . . . . . . . . . . . . . 18 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} = ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})
140	139	ineq2i 4176	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
141		indi 4243	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}))
142	140, 141	eqtr2i 2793	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
143		un0 4356	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∪ ∅) = ∅
144	138, 142, 143	3eqtr3g 2827	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
145	113, 144	eqtrid 2816	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅)
146		fnimadisj 6668	. . . . . . . . . . . . . 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 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
148	39	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
149		elfzuz3 13549	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑦))
150		peano2uz 12925	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
151	149, 150	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
152	151	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
153	148, 152	eqeltrrd 2870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘𝑦))
154		fzss2 13592	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑦) → (1...𝑦) ⊆ (1...𝑁))
155		reldisj 4417	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ⊆ (1...𝑁) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
156	153, 154, 155	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
157	156	adantr 485	. . . . . . . . . . . . . . 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 6079	. . . . . . . . . . . . . 14 ⊢ ((1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
160	158, 159	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
161	147, 160	uneq12d 4129	. . . . . . . . . . . 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 6149	. . . . . . . . . . . 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 4118	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
164		un0 4356	. . . . . . . . . . . . 13 ⊢ ((1...𝑦) ∪ ∅) = (1...𝑦)
165	163, 164	eqtr2i 2793	. . . . . . . . . . . 12 ⊢ (1...𝑦) = (∅ ∪ (1...𝑦))
166	161, 162, 165	3eqtr4g 2829	. . . . . . . . . . 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 6063	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
168	109, 167	eqtrid 2816	. . . . . . . . 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 5691	. . . . . . . 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 6253	. . . . . . . . . 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 6149	. . . . . . . . . . . . 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 6074	. . . . . . . . . . . . . . . . 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 6666	. . . . . . . . . . . . . . . . . . 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 19	. . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . 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 13552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
178		zltp1le 12644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℤ ∧ (2^nd ‘𝑇) ∈ ℤ) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
179	177, 57, 178	syl2anr 608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
180	179	biimpa 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ (2^nd ‘𝑇))
181	18, 52, 56	ltled 11358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ 𝑁)
182	181	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑁)
183	57	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ ℤ)
184		nn0p1nn 12543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ ℕ)
185	114, 184	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
186	185	nnzd 12617	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
187	186	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
188	40	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
189		elfz 13541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
190	183, 187, 188, 189	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
191	190	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
192	180, 182, 191	mpbir2and 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁))
193		1red 11209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 1 ∈ ℝ)
194		ltle 11298	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
195	115, 18, 194	syl2anr 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
196	195	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ≤ (2^nd ‘𝑇))
197	123, 124, 193, 196	leadd1dd 11828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1))
198	60	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
199	57	peano2zd 12703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℤ)
200	199	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ ℤ)
201		elfz 13541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
202	200, 187, 188, 201	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
203	202	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
204	197, 198, 203	mpbir2and 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
205		prssi 4789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
206	192, 204, 205	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207		imass2 6105	. . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . 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 3978	. . . . . . . . . . . . . . . 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 3960	. . . . . . . . . . . . . . 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 6829	. . . . . . . . . . . . . . . . . 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 6796	. . . . . . . . . . . . . . . . . 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 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
214	213, 27	eqtrdi 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
215	214	ad2antrr 738	. . . . . . . . . . . . . . 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 2804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
217		undif 4446	. . . . . . . . . . . . . . . . 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 6063	. . . . . . . . . . . . . . 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 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
221		disjdifr 4437	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅
222		fnimadisj 6668	. . . . . . . . . . . . . . . . . . 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 704	. . . . . . . . . . . . . . . . . 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 12901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
226	185, 225	eleqtrdi 2879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ_≥‘1))
227		fzss1 13591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
228	226, 227	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
229	228	ssdifd 4105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
230		resiima 6079	. . . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . . 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 739	. . . . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . 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 6148	. . . . . . . . . . . . . . . 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 4118	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
236		un0 4356	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
237	235, 236	eqtr2i 2793	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
238	233, 234, 237	3eqtr4g 2829	. . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
240	216, 239	uneq12d 4129	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
241	171, 240	eqtrid 2816	. . . . . . . . . . . 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 2804	. . . . . . . . . . 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 6063	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
244	170, 243	eqtrid 2816	. . . . . . . . 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 5691	. . . . . . . 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 4129	. . . . . . 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 7427	. . . . . 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 4496	. . . . . . . . 9 ⊢ (𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
249	248	csbeq1d 3863	. . . . . . . 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 3465	. . . . . . . . 9 ⊢ 𝑦 ∈ V
251		oveq2 7419	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
252	251	imaeq2d 6063	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 7418	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
255	254	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
256	255	imaeq2d 6063	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 4129	. . . . . . . . . 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 7427	. . . . . . . . 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 3894	. . . . . . . 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 2820	. . . . . . 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 486	. . . . . 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 3863	. . . . . . . 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 6063	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
265	264	xpeq1d 5691	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
266	255	imaeq2d 6063	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
267	266	xpeq1d 5691	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
268	265, 267	uneq12d 4129	. . . . . . . . . 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 7427	. . . . . . . . 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 3894	. . . . . . . 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 2820	. . . . . . 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 486	. . . . . 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 2814	. . . . 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 11288	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
275	18, 115, 274	syl2an 607	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
276	275	biimpar 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑦)
277		imaco 6253	. . . . . . . . . . 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 6149	. . . . . . . . . . . . . 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 6074	. . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℕ)
283	18	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℝ)
284	115	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
285	185	nnred 12248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
286	285	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
287		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
288	115	lep1d 12146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
289	288	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
290	283, 284, 286, 287, 289	letrd 11367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ (𝑦 + 1))
291		fznn 13620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
292	186, 291	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
293	292	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
294	282, 290, 293	mpbir2and 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ (1...(𝑦 + 1)))
295	50	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℕ)
296		1red 11209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 1 ∈ ℝ)
297	283, 284, 296, 287	leadd1dd 11828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))
298		fznn 13620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
299	186, 298	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
300	299	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
301	295, 297, 300	mpbir2and 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)))
302		prssi 4789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
303	294, 301, 302	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
304		imass2 6105	. . . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . . 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 3978	. . . . . . . . . . . . . . . . 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 3960	. . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . 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 2804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
310		undif 4446	. . . . . . . . . . . . . . . . . 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 6063	. . . . . . . . . . . . . . . 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 12890	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
315	149, 314	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
316	315	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
317	148, 316	eqeltrrd 2870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑦 + 1)))
318		fzss2 13592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
319	317, 318	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
320	319	ssdifd 4105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
321	320	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
322		resiima 6079	. . . . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . . 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 6148	. . . . . . . . . . . . . . . . 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 4118	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
327		un0 4356	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
328	326, 327	eqtr2i 2793	. . . . . . . . . . . . . . . . 17 ⊢ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
329	324, 325, 328	3eqtr4g 2829	. . . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) ∪ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...(𝑦 + 1)))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
332	278, 331	eqtrid 2816	. . . . . . . . . . . . 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 2804	. . . . . . . . . . . 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 6063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1)))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
335	277, 334	eqtrid 2816	. . . . . . . . . 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 5691	. . . . . . . . 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 6253	. . . . . . . . . . 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 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
339		incom 4168	. . . . . . . . . . . . . . . 16 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
340	125	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
341	185	peano2nnd 12250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
342	341	nnred 12248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
343	342	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
344	19	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
345	115	ltp1d 12145	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
346	345	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
347	283, 284, 286, 287, 346	lelttrd 11368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < (𝑦 + 1))
348	283, 286, 296, 347	ltadd1dd 11825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1))
349	283, 340, 343, 344, 348	lttrd 11371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((𝑦 + 1) + 1))
350		ltnle 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
351	18, 342, 350	syl2an 607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
352	351	adantr 485	. . . . . . . . . . . . . . . . . . . . 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 13555	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
355	353, 354	nsyl 141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
356		disjsn 4680	. . . . . . . . . . . . . . . . . . 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 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
359	125, 342, 358	syl2an 607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
360	359	adantr 485	. . . . . . . . . . . . . . . . . . . . 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 13555	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
363	361, 362	nsyl 141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
364		disjsn 4680	. . . . . . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
367	139	ineq2i 4176	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
368		indi 4243	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}))
369	367, 368	eqtr2i 2793	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
370	366, 369, 143	3eqtr3g 2827	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
371	339, 370	eqtrid 2816	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
372		fnimadisj 6668	. . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
374	341, 225	eleqtrdi 2879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ_≥‘1))
375		fzss1 13591	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 + 1) + 1) ∈ (ℤ_≥‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
376		reldisj 4417	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
377	374, 375, 376	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
378	377	ad2antlr 739	. . . . . . . . . . . . . . . 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 6079	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
381	379, 380	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
382	373, 381	uneq12d 4129	. . . . . . . . . . . . 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 6149	. . . . . . . . . . . . 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 4118	. . . . . . . . . . . . . 14 ⊢ (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
385		un0 4356	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
386	384, 385	eqtr2i 2793	. . . . . . . . . . . . 13 ⊢ (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
387	382, 383, 386	3eqtr4g 2829	. . . . . . . . . . . 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 6063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘(1^st ‘𝑇)) “ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
389	337, 388	eqtrid 2816	. . . . . . . . . 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 5691	. . . . . . . . 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 4129	. . . . . . . 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 602	. . . . . . 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 7427	. . . . . 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 4499	. . . . . . . . 9 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
395	394	csbeq1d 3863	. . . . . . . 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 7444	. . . . . . . . 9 ⊢ (𝑦 + 1) ∈ V
397		oveq2 7419	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
398	397	imaeq2d 6063	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 7418	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
401	400	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
402	401	imaeq2d 6063	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 4129	. . . . . . . . . 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 7427	. . . . . . . . 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 3894	. . . . . . . 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 2820	. . . . . . 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 486	. . . . . 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 3863	. . . . . . . 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 6063	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
411	410	xpeq1d 5691	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}))
412	401	imaeq2d 6063	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
413	412	xpeq1d 5691	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
414	411, 413	uneq12d 4129	. . . . . . . . . 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 7427	. . . . . . . . 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 3894	. . . . . . . 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 2820	. . . . . . 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 486	. . . . . 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 2814	. . . . 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 824	. . . 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 5206	. . 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 2807	. 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 5446	. . . . . . 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 7996	. . . . . 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 7997	. . . . . 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 5115	. . . . . . . . 9 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
427	426	ifbid 4514	. . . . . . . 8 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
428	427	csbeq1d 3863	. . . . . . 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 6895	. . . . . . . . . 10 ⊢ (1^st ‘(1^st ‘𝑇)) ∈ V
430	429, 79	op1std 7996	. . . . . . . . 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 7997	. . . . . . . . 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 23	. . . . . . . . . 10 ⊢ ((1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)) → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
433		imaeq1 6058	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 6058	. . . . . . . . . . . 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 5691	. . . . . . . . . . 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 4129	. . . . . . . . . 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 7430	. . . . . . . . 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 595	. . . . . . . 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 3866	. . . . . . 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 2826	. . . . . 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 595	. . . . 5 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
443	442	mpteq2dv 5207	. . . 4 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))))
444	443	eqeq2d 2780	. . 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 3661	. 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 594	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 400 = wceq 1567 ∈ wcel 2149 {cab 2747 ≠ wne 2964 {crab 3422 Vcvv 3461 ⦋csb 3859 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 ifcif 4490 {csn 4592 {cpr 4594 ⟨cop 4598 class class class wbr 5111 ↦ cmpt 5194 I cid 5556 × cxp 5660 ran crn 5663 ↾ cres 5664 “ cima 5665 ∘ ccom 5666 Fn wfn 6532 ⟶wf 6533 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7411 ∘_f cof 7673 1^st c1st 7984 2^nd c2nd 7985 ↑_m cmap 8824 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 < clt 11243 ≤ cle 11244 − cmin 11441 ℕcn 12233 ℕ₀cn0 12504 ℤcz 12591 ℤ_≥cuz 12862 ...cfz 13535 ..^cfzo 13682

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536

This theorem is referenced by: poimirlem22 38216

W3C validator