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 35792

Description: Lemma for poimir 35810, that the face in poimirlem22 35799 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 3618	. . . . . . 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 2857	. . . . . 6 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5	1, 4	syl 17	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6		xp1st 7863	. . . . 5 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7		xp1st 7863	. . . . 5 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
8	5, 6, 7	3syl 18	. . . 4 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
9		xp2nd 7864	. . . . . . . 8 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10	5, 6, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11		fvex 6787	. . . . . . . 8 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6704	. . . . . . . 8 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3609	. . . . . . 7 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 217	. . . . . 6 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		poimirlem15.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
16		elfznn 13285	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
17	15, 16	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
18	17	nnred 11988	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
19	18	ltp1d 11905	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
20	18, 19	ltned 11111	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
21	20	necomd 2999	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇))
22		fvex 6787	. . . . . . . . . . 11 ⊢ (2^nd ‘𝑇) ∈ V
23		ovex 7308	. . . . . . . . . . 11 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
24		f1oprg 6761	. . . . . . . . . . 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 690	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≠ (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
26	20, 21, 25	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
27		prcom 4668	. . . . . . . . . 10 ⊢ {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
28		f1oeq3 6706	. . . . . . . . . 10 ⊢ ({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
29	27, 28	ax-mp 5	. . . . . . . . 9 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ↔ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
30	26, 29	sylib 217	. . . . . . . 8 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
31		f1oi 6754	. . . . . . . 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 4405	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
33		f1oun 6735	. . . . . . . . 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 702	. . . . . . . 8 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
35	30, 31, 34	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
36		poimir.0	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
37	36	nncnd 11989	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
38		npcan1 11400	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
39	37, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
40	36	nnzd 12425	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
41		peano2zm 12363	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
42	40, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
43		uzid 12597	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
44		peano2uz 12641	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
45	42, 43, 44	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
46	39, 45	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
47		fzss2 13296	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
49	48, 15	sseldd 3922	. . . . . . . . . 10 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...𝑁))
50	17	peano2nnd 11990	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℕ)
51	42	zred 12426	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
52	36	nnred 11988	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
53		elfzle2 13260	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≤ (𝑁 − 1))
54	15, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ (𝑁 − 1))
55	52	ltm1d 11907	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
56	18, 51, 52, 54, 55	lelttrd 11133	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘𝑇) < 𝑁)
57	17	nnzd 12425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℤ)
58		zltp1le 12370	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
59	57, 40, 58	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘𝑇) < 𝑁 ↔ ((2^nd ‘𝑇) + 1) ≤ 𝑁))
60	56, 59	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
61		fznn 13324	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
62	40, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ∈ (1...𝑁) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
63	50, 60, 62	mpbir2and 710	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
64		prssi 4754	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
65	49, 63, 64	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁))
66		undif 4415	. . . . . . . . 9 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
67	65, 66	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁))
68		f1oeq23 6707	. . . . . . . 8 ⊢ ((({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁) ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...𝑁)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ↔ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
69	67, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))–1-1-onto→({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ↔ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
70	35, 69	mpbid 231	. . . . . 6 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁))
71		f1oco 6739	. . . . . 6 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
72	14, 70, 71	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
73		prex 5355	. . . . . . . 8 ⊢ {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∈ V
74		ovex 7308	. . . . . . . . 9 ⊢ (1...𝑁) ∈ V
75		difexg 5251	. . . . . . . . 9 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∈ V)
76		resiexg 7761	. . . . . . . . 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 7596	. . . . . . 7 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) ∈ V
79	11, 78	coex 7777	. . . . . 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 6704	. . . . . 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 3609	. . . . 5 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
82	72, 81	sylibr 233	. . . 4 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
83		opelxpi 5626	. . . 4 ⊢ (((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) ∧ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
84	8, 82, 83	syl2anc 584	. . 3 ⊢ (𝜑 → ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
85		fz1ssfz0 13352	. . . . 5 ⊢ (1...𝑁) ⊆ (0...𝑁)
86	48, 85	sstrdi 3933	. . . 4 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
87	86, 15	sseldd 3922	. . 3 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
88		opelxpi 5626	. . 3 ⊢ ((⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (2^nd ‘𝑇) ∈ (0...𝑁)) → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
89	84, 87, 88	syl2anc 584	. 2 ⊢ (𝜑 → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
90		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
91	90	breq2d 5086	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
92	91	ifbid 4482	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
93	92	csbeq1d 3836	. . . . . . . . 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 6779	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
95		2fveq3 6779	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
96	95	imaeq1d 5968	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
97	96	xpeq1d 5618	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
98	95	imaeq1d 5968	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
99	98	xpeq1d 5618	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
100	97, 99	uneq12d 4098	. . . . . . . . . . 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 7293	. . . . . . . . . 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 3839	. . . . . . . . 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 2778	. . . . . . . 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 5176	. . . . . . 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 2749	. . . . . 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 3627	. . . . 5 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
107	106	simprbi 497	. . . 4 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
108	1, 107	syl 17	. . 3 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
109		imaco 6155	. . . . . . . . . 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 6717	. . . . . . . . . . . . . . . 16 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–1-1-onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
111	26, 110	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
112	111	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
113		incom 4135	. . . . . . . . . . . . . . 15 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
114		elfznn0 13349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ₀)
115	114	nn0red 12294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
116		ltnle 11054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
117	115, 18, 116	syl2anr 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ ¬ (2^nd ‘𝑇) ≤ 𝑦))
118	117	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ≤ 𝑦)
119		elfzle2 13260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ (1...𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
120	118, 119	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
121		disjsn 4647	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (1...𝑦))
122	120, 121	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇)}) = ∅)
123	115	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ∈ ℝ)
124	18	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ℝ)
125	50	nnred 11988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℝ)
126	125	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
127		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < (2^nd ‘𝑇))
128	19	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
129	123, 124, 126, 127, 128	lttrd 11136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 < ((2^nd ‘𝑇) + 1))
130		ltnle 11054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ ((2^nd ‘𝑇) + 1) ∈ ℝ) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
131	115, 125, 130	syl2anr 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
132	131	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 < ((2^nd ‘𝑇) + 1) ↔ ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦))
133	129, 132	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ≤ 𝑦)
134		elfzle2 13260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) + 1) ∈ (1...𝑦) → ((2^nd ‘𝑇) + 1) ≤ 𝑦)
135	133, 134	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
136		disjsn 4647	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (1...𝑦))
137	135, 136	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
138	122, 137	uneq12d 4098	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
139		df-pr 4564	. . . . . . . . . . . . . . . . . 18 ⊢ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} = ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})
140	139	ineq2i 4143	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
141		indi 4207	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)}))
142	140, 141	eqtr2i 2767	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑦) ∩ {(2^nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2^nd ‘𝑇) + 1)})) = ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
143		un0 4324	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∪ ∅) = ∅
144	138, 142, 143	3eqtr3g 2801	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
145	113, 144	eqtrid 2790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅)
146		fnimadisj 6565	. . . . . . . . . . . . . 14 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ∅) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
147	112, 145, 146	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...𝑦)) = ∅)
148	39	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
149		elfzuz3 13253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑦))
150		peano2uz 12641	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
151	149, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
152	151	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
153	148, 152	eqeltrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘𝑦))
154		fzss2 13296	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑦) → (1...𝑦) ⊆ (1...𝑁))
155		reldisj 4385	. . . . . . . . . . . . . . . . 17 ⊢ ((1...𝑦) ⊆ (1...𝑁) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
156	153, 154, 155	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
157	156	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((1...𝑦) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
158	144, 157	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
159		resiima 5984	. . . . . . . . . . . . . 14 ⊢ ((1...𝑦) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
160	158, 159	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
161	147, 160	uneq12d 4098	. . . . . . . . . . . 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 6054	. . . . . . . . . . . 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 4087	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
164		un0 4324	. . . . . . . . . . . . 13 ⊢ ((1...𝑦) ∪ ∅) = (1...𝑦)
165	163, 164	eqtr2i 2767	. . . . . . . . . . . 12 ⊢ (1...𝑦) = (∅ ∪ (1...𝑦))
166	161, 162, 165	3eqtr4g 2803	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...𝑦)) = (1...𝑦))
167	166	imaeq2d 5969	. . . . . . . . . 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 2790	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
169	168	xpeq1d 5618	. . . . . . . 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 6155	. . . . . . . . . 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 6054	. . . . . . . . . . . . 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 5980	. . . . . . . . . . . . . . . . 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 6563	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
175	26, 110, 174	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩})
176	175	ad2antrr 723	. . . . . . . . . . . . . . . . 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 13256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
178		zltp1le 12370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℤ ∧ (2^nd ‘𝑇) ∈ ℤ) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
179	177, 57, 178	syl2anr 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2^nd ‘𝑇)))
180	179	biimpa 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ (2^nd ‘𝑇))
181	18, 52, 56	ltled 11123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2^nd ‘𝑇) ≤ 𝑁)
182	181	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑁)
183	57	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ ℤ)
184		nn0p1nn 12272	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ ℕ)
185	114, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
186	185	nnzd 12425	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
187	186	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
188	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
189		elfz 13245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
190	183, 187, 188, 189	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
191	190	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2^nd ‘𝑇) ∧ (2^nd ‘𝑇) ≤ 𝑁)))
192	180, 182, 191	mpbir2and 710	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁))
193		1red 10976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 1 ∈ ℝ)
194		ltle 11063	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℝ ∧ (2^nd ‘𝑇) ∈ ℝ) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
195	115, 18, 194	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2^nd ‘𝑇) → 𝑦 ≤ (2^nd ‘𝑇)))
196	195	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → 𝑦 ≤ (2^nd ‘𝑇))
197	123, 124, 193, 196	leadd1dd 11589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1))
198	60	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ≤ 𝑁)
199	57	peano2zd 12429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℤ)
200	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ ℤ)
201		elfz 13245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
202	200, 187, 188, 201	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
203	202	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2^nd ‘𝑇) + 1) ∧ ((2^nd ‘𝑇) + 1) ≤ 𝑁)))
204	197, 198, 203	mpbir2and 710	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
205		prssi 4754	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2^nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
206	192, 204, 205	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207		imass2 6010	. . . . . . . . . . . . . . . . . 18 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
208	206, 207	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
209	176, 208	eqsstrrd 3960	. . . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . . . 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 6723	. . . . . . . . . . . . . . . . . 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 6691	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}–onto→{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
213	26, 211, 212	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
214	213, 27	eqtrdi 2794	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
215	214	ad2antrr 723	. . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
217		undif 4415	. . . . . . . . . . . . . . . . 17 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
218	206, 217	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
219	218	imaeq2d 5969	. . . . . . . . . . . . . . 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 6561	. . . . . . . . . . . . . . . . . . 19 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
221		disjdifr 4406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅
222		fnimadisj 6565	. . . . . . . . . . . . . . . . . . 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 689	. . . . . . . . . . . . . . . . . 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 12621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
226	185, 225	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ_≥‘1))
227		fzss1 13295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
228	226, 227	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
229	228	ssdifd 4075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
230		resiima 5984	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
231	229, 230	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
232	231	ad2antlr 724	. . . . . . . . . . . . . . . . 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 4098	. . . . . . . . . . . . . . . 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 6053	. . . . . . . . . . . . . . . 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 4087	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
236		un0 4324	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
237	235, 236	eqtr2i 2767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
238	233, 234, 237	3eqtr4g 2803	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
239	219, 238	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
240	216, 239	uneq12d 4098	. . . . . . . . . . . . 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 2790	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
242	241, 218	eqtrd 2778	. . . . . . . . . . 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 5969	. . . . . . . . . 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 2790	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
245	244	xpeq1d 5618	. . . . . . . 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 4098	. . . . . . 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 7291	. . . . . 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 4465	. . . . . . . . 9 ⊢ (𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
249	248	csbeq1d 3836	. . . . . . . 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 3436	. . . . . . . . 9 ⊢ 𝑦 ∈ V
251		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
252	251	imaeq2d 5969	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 7282	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
255	254	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
256	255	imaeq2d 5969	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 4098	. . . . . . . . . 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 7291	. . . . . . . . 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 3868	. . . . . . . 8 ⊢ ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})))
261	249, 260	eqtrdi 2794	. . . . . . 7 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
262	261	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
263	248	csbeq1d 3836	. . . . . . . 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 5969	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
265	264	xpeq1d 5618	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
266	255	imaeq2d 5969	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
267	266	xpeq1d 5618	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
268	265, 267	uneq12d 4098	. . . . . . . . . 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 7291	. . . . . . . . 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 3868	. . . . . . . 8 ⊢ ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
271	263, 270	eqtrdi 2794	. . . . . . 7 ⊢ (𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
272	271	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
273	247, 262, 272	3eqtr4d 2788	. . . . 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 11053	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
275	18, 115, 274	syl2an 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2^nd ‘𝑇)))
276	275	biimpar 478	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (2^nd ‘𝑇) ≤ 𝑦)
277		imaco 6155	. . . . . . . . . . 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 6054	. . . . . . . . . . . . . 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 5980	. . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℕ)
283	18	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ ℝ)
284	115	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
285	185	nnred 11988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
286	285	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
287		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ 𝑦)
288	115	lep1d 11906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
289	288	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
290	283, 284, 286, 287, 289	letrd 11132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ≤ (𝑦 + 1))
291		fznn 13324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
292	186, 291	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
293	292	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2^nd ‘𝑇) ∈ ℕ ∧ (2^nd ‘𝑇) ≤ (𝑦 + 1))))
294	282, 290, 293	mpbir2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) ∈ (1...(𝑦 + 1)))
295	50	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℕ)
296		1red 10976	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 1 ∈ ℝ)
297	283, 284, 296, 287	leadd1dd 11589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))
298		fznn 13324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + 1) ∈ ℤ → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
299	186, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
300	299	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2^nd ‘𝑇) + 1) ∈ ℕ ∧ ((2^nd ‘𝑇) + 1) ≤ (𝑦 + 1))))
301	295, 297, 300	mpbir2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1)))
302		prssi 4754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
303	294, 301, 302	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
304		imass2 6010	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))))
305	303, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))))
306	281, 305	eqsstrrd 3960	. . . . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (1...(𝑦 + 1))) = {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
310		undif 4415	. . . . . . . . . . . . . . . . . 18 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) ↔ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...(𝑦 + 1)))
311	303, 310	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (1...(𝑦 + 1)))
312	311	imaeq2d 5969	. . . . . . . . . . . . . . . 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 12610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
315	149, 314	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
316	315	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
317	148, 316	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑦 + 1)))
318		fzss2 13296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
319	317, 318	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
320	319	ssdifd 4075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
321	320	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
322		resiima 5984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
323	321, 322	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
324	313, 323	uneq12d 4098	. . . . . . . . . . . . . . . . 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 6053	. . . . . . . . . . . . . . . . 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 4087	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅)
327		un0 4324	. . . . . . . . . . . . . . . . . 18 ⊢ (((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
328	326, 327	eqtr2i 2767	. . . . . . . . . . . . . . . . 17 ⊢ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
329	324, 325, 328	3eqtr4g 2803	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) = ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
330	312, 329	eqtr3d 2780	. . . . . . . . . . . . . . 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 4098	. . . . . . . . . . . . . 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 2790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (1...(𝑦 + 1))) = ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
333	332, 311	eqtrd 2778	. . . . . . . . . . . 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 5969	. . . . . . . . . . 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 2790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
336	335	xpeq1d 5618	. . . . . . . . 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 6155	. . . . . . . . . . 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 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
339		incom 4135	. . . . . . . . . . . . . . . 16 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
340	125	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) ∈ ℝ)
341	185	peano2nnd 11990	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
342	341	nnred 11988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
343	342	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
344	19	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
345	115	ltp1d 11905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
346	345	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
347	283, 284, 286, 287, 346	lelttrd 11133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < (𝑦 + 1))
348	283, 286, 296, 347	ltadd1dd 11586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1))
349	283, 340, 343, 344, 348	lttrd 11136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (2^nd ‘𝑇) < ((𝑦 + 1) + 1))
350		ltnle 11054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
351	18, 342, 350	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
352	351	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((2^nd ‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇)))
353	349, 352	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
354		elfzle1 13259	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2^nd ‘𝑇))
355	353, 354	nsyl 140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
356		disjsn 4647	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅ ↔ ¬ (2^nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
357	355, 356	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) = ∅)
358		ltnle 11054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
359	125, 342, 358	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
360	359	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1)))
361	348, 360	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
362		elfzle1 13259	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2^nd ‘𝑇) + 1))
363	361, 362	nsyl 140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
364		disjsn 4647	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅ ↔ ¬ ((2^nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
365	363, 364	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}) = ∅)
366	357, 365	uneq12d 4098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = (∅ ∪ ∅))
367	139	ineq2i 4143	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)}))
368		indi 4207	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2^nd ‘𝑇)} ∪ {((2^nd ‘𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)}))
369	367, 368	eqtr2i 2767	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2^nd ‘𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
370	366, 369, 143	3eqtr3g 2801	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅)
371	339, 370	eqtrid 2790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
372		fnimadisj 6565	. . . . . . . . . . . . . . 15 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
373	338, 371, 372	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
374	341, 225	eleqtrdi 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ_≥‘1))
375		fzss1 13295	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 + 1) + 1) ∈ (ℤ_≥‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
376		reldisj 4385	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
377	374, 375, 376	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
378	377	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
379	370, 378	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
380		resiima 5984	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
381	379, 380	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
382	373, 381	uneq12d 4098	. . . . . . . . . . . . 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 6054	. . . . . . . . . . . . 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 4087	. . . . . . . . . . . . . 14 ⊢ (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
385		un0 4324	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
386	384, 385	eqtr2i 2767	. . . . . . . . . . . . 13 ⊢ (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
387	382, 383, 386	3eqtr4g 2803	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
388	387	imaeq2d 5969	. . . . . . . . . . 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 2790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
390	389	xpeq1d 5618	. . . . . . . . 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 4098	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2^nd ‘𝑇) ≤ 𝑦) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
392	276, 391	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
393	392	oveq2d 7291	. . . . . 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 4468	. . . . . . . . 9 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
395	394	csbeq1d 3836	. . . . . . . 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 7308	. . . . . . . . 9 ⊢ (𝑦 + 1) ∈ V
397		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
398	397	imaeq2d 5969	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 7282	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
401	400	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
402	401	imaeq2d 5969	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 4098	. . . . . . . . . 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 7291	. . . . . . . . 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 3868	. . . . . . . 8 ⊢ ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
407	395, 406	eqtrdi 2794	. . . . . . 7 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
408	407	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
409	394	csbeq1d 3836	. . . . . . . 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 5969	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))))
411	410	xpeq1d 5618	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}))
412	401	imaeq2d 5969	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
413	412	xpeq1d 5618	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
414	411, 413	uneq12d 4098	. . . . . . . . . 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 7291	. . . . . . . . 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 3868	. . . . . . . 8 ⊢ ⦋(𝑦 + 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
417	409, 416	eqtrdi 2794	. . . . . . 7 ⊢ (¬ 𝑦 < (2^nd ‘𝑇) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
418	417	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
419	393, 408, 418	3eqtr4d 2788	. . . . 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 810	. . . 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 5174	. . 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 2781	. 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 5379	. . . . . . 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 7841	. . . . . 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 7842	. . . . . 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 5078	. . . . . . . . 9 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
427	426	ifbid 4482	. . . . . . . 8 ⊢ ((2^nd ‘𝑡) = (2^nd ‘𝑇) → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
428	427	csbeq1d 3836	. . . . . . 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 6787	. . . . . . . . . 10 ⊢ (1^st ‘(1^st ‘𝑇)) ∈ V
430	429, 79	op1std 7841	. . . . . . . . 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 7842	. . . . . . . . 9 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
432		id 22	. . . . . . . . . 10 ⊢ ((1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)) → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
433		imaeq1 5964	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 5964	. . . . . . . . . . . 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 5618	. . . . . . . . . . 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 4098	. . . . . . . . . 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 7294	. . . . . . . . 9 ⊢ (((1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
439	430, 431, 438	syl2anc 584	. . . . . . . 8 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
440	439	csbeq2dv 3839	. . . . . . 7 ⊢ ((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
441	428, 440	sylan9eqr 2800	. . . . . 6 ⊢ (((1^st ‘𝑡) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∧ (2^nd ‘𝑡) = (2^nd ‘𝑇)) → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
442	424, 425, 441	syl2anc 584	. . . . 5 ⊢ (𝑡 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
443	442	mpteq2dv 5176	. . . 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 2749	. . 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 3627	. 2 ⊢ (⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆 ↔ (⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + (((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
446	89, 422, 445	sylanbrc 583	1 ⊢ (𝜑 → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 {cab 2715 ≠ wne 2943 {crab 3068 Vcvv 3432 ⦋csb 3832 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 ifcif 4459 {csn 4561 {cpr 4563 ⟨cop 4567 class class class wbr 5074 ↦ cmpt 5157 I cid 5488 × cxp 5587 ran crn 5590 ↾ cres 5591 “ cima 5592 ∘ ccom 5593 Fn wfn 6428 ⟶wf 6429 –onto→wfo 6431 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 ∘_f cof 7531 1^st c1st 7829 2^nd c2nd 7830 ↑_m cmap 8615 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 < clt 11009 ≤ cle 11010 − cmin 11205 ℕcn 11973 ℕ₀cn0 12233 ℤcz 12319 ℤ_≥cuz 12582 ...cfz 13239 ..^cfzo 13382

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-fz 13240

This theorem is referenced by: poimirlem22 35799

W3C validator