poimirlem11 - Mathbox for Brendan Leahy

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

Theorem poimirlem11 32590

Description: Lemma for poimir 32612 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimirlem22.s	⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1	⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
poimirlem12.2	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem11.3	⊢ (𝜑 → (2^nd ‘𝑇) = 0)
poimirlem11.4	⊢ (𝜑 → 𝑈 ∈ 𝑆)
poimirlem11.5	⊢ (𝜑 → (2^nd ‘𝑈) = 0)
poimirlem11.6	⊢ (𝜑 → 𝑀 ∈ (1...𝑁))

**Assertion**
Ref	Expression
poimirlem11	⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

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

**Proof of Theorem poimirlem11**
Step	Hyp	Ref	Expression
1		eldif 3550	. . . . . . 7 ⊢ (𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
2		imassrn 5396	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ran (2^nd ‘(1^st ‘𝑇))
3		poimirlem12.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
4		elrabi 3328	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5		poimirlem22.s	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
6	4, 5	eleq2s 2706	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7	3, 6	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
8		xp1st 7089	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9	7, 8	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
10		xp2nd 7090	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11	9, 10	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
12		fvex 6113	. . . . . . . . . . . . . . . 16 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
13		f1oeq1 6040	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
14	12, 13	elab 3319	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15	11, 14	sylib 207	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
16		f1of 6050	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
17	15, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
18		frn 5966	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
19	17, 18	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
20	2, 19	syl5ss 3579	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
21		poimirlem11.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
22		elrabi 3328	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
23	22, 5	eleq2s 2706	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
24	21, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
25		xp1st 7089	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
26	24, 25	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
27		xp2nd 7090	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
28	26, 27	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
29		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
30		f1oeq1 6040	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
31	29, 30	elab 3319	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
32	28, 31	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
33		f1ofo 6057	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
35		foima 6033	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
37	20, 36	sseqtr4d 3605	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)))
38	37	ssdifd 3708	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
39		dff1o3 6056	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑈))))
40	39	simprbi 479	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
41	32, 40	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
42		imadif 5887	. . . . . . . . . . 11 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
43	41, 42	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
44		difun2 4000	. . . . . . . . . . . 12 ⊢ ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
45		poimirlem11.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
46		fzsplit 12238	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
47	45, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
48		uncom 3719	. . . . . . . . . . . . . 14 ⊢ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
49	47, 48	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
50	49	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
51		incom 3767	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
52		elfznn 12241	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ)
53	45, 52	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ)
54	53	nnred 10912	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
55	54	ltp1d 10833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
56		fzdisj 12239	. . . . . . . . . . . . . . 15 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
57	55, 56	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
58	51, 57	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
59		disj3 3973	. . . . . . . . . . . . 13 ⊢ ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
60	58, 59	sylib 207	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
61	44, 50, 60	3eqtr4a 2670	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
62	61	imaeq2d 5385	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
63	43, 62	eqtr3d 2646	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
64	38, 63	sseqtrd 3604	. . . . . . . 8 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
65	64	sselda 3568	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
66	1, 65	sylan2br 492	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
67		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (2^nd ‘𝑡) = (2^nd ‘𝑈))
68	67	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑈)))
69	68	ifbid 4058	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)))
70	69	csbeq1d 3506	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑈 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
71		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (1^st ‘𝑡) = (1^st ‘𝑈))
72	71	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑈)))
73	71	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑈 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑈)))
74	73	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)))
75	74	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}))
76	73	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)))
77	76	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
78	75, 77	uneq12d 3730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))
79	72, 78	oveq12d 6567	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
80	79	csbeq2dv 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑈 → ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
81	70, 80	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑈 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
82	81	mpteq2dv 4673	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑈 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
83	82	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑈 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
84	83, 5	elrab2 3333	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
85	84	simprbi 479	. . . . . . . . . . 11 ⊢ (𝑈 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
86	21, 85	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
87		poimirlem11.5	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘𝑈) = 0)
88		breq12 4588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = (𝑀 − 1) ∧ (2^nd ‘𝑈) = 0) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
89	87, 88	sylan2 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
90	89	ancoms 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
91		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
92	53	nncnd 10913	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℂ)
93		npcan1 10334	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
94	92, 93	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
95	91, 94	sylan9eqr 2666	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
96	90, 95	ifbieq2d 4061	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
97	53	nnzd 11357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		poimir.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
99	98	nnzd 11357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℤ)
100		elfzm1b 12287	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
101	97, 99, 100	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
102	45, 101	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
103		elfzle1 12215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) → 0 ≤ (𝑀 − 1))
104	102, 103	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝑀 − 1))
105		0red 9920	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
106		nnm1nn0 11211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ₀)
107	53, 106	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ₀)
108	107	nn0red 11229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
109	105, 108	lenltd 10062	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < 0))
110	104, 109	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ (𝑀 − 1) < 0)
111	110	iffalsed 4047	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
112	111	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
113	96, 112	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
114	113	csbeq1d 3506	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
115		oveq2 6557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
116	115	imaeq2d 5385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
117	116	xpeq1d 5062	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}))
118		oveq1 6556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
119	118	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
120	119	imaeq2d 5385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
121	120	xpeq1d 5062	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
122	117, 121	uneq12d 3730	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑀 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))
123	122	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑀 → ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
124	123	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
125	45, 124	csbied 3526	. . . . . . . . . . . 12 ⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
126	125	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
127	114, 126	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
128		ovex 6577	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V
129	128	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
130	86, 127, 102, 129	fvmptd 6197	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
131	130	fveq1d 6105	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
132	131	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
133		imassrn 5396	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2^nd ‘(1^st ‘𝑈))
134		f1of 6050	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
135	32, 134	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
136		frn 5966	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
137	135, 136	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
138	133, 137	syl5ss 3579	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
139	138	sselda 3568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
140		xp1st 7089	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
141	26, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
142		elmapfn 7766	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
143	141, 142	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
144	143	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
145		1ex 9914	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
146		fnconstg 6006	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
147	145, 146	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))
148		c0ex 9913	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
149		fnconstg 6006	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
150	148, 149	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))
151	147, 150	pm3.2i 470	. . . . . . . . . . . 12 ⊢ ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
152		imain 5888	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
153	41, 152	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
154	57	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑈)) “ ∅))
155		ima0 5400	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ∅) = ∅
156	154, 155	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
157	153, 156	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
158		fnun 5911	. . . . . . . . . . . 12 ⊢ ((((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
159	151, 157, 158	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
160		imaundi 5464	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
161	47	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
162	161, 36	eqtr3d 2646	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
163	160, 162	syl5eqr 2658	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
164	163	fneq2d 5896	. . . . . . . . . . 11 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
165	159, 164	mpbid 221	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
166	165	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
167		ovex 6577	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ V
168	167	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
169		inidm 3784	. . . . . . . . 9 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
170		eqidd 2611	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
171		fvun2 6180	. . . . . . . . . . . . 13 ⊢ (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
172	147, 150, 171	mp3an12 1406	. . . . . . . . . . . 12 ⊢ (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
173	157, 172	sylan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
174	148	fvconst2 6374	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
175	174	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
176	173, 175	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
177	176	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
178	144, 166, 168, 168, 169, 170, 177	ofval 6804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0))
179	139, 178	mpdan 699	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0))
180		elmapi 7765	. . . . . . . . . . . . 13 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
181	141, 180	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
182	181	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾))
183		elfzonn0 12380	. . . . . . . . . . 11 ⊢ (((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
184	182, 183	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
185	184	nn0cnd 11230	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
186	139, 185	syldan 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
187	186	addid1d 10115	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
188	132, 179, 187	3eqtrd 2648	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
189	66, 188	syldan 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
190		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
191	190	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
192	191	ifbid 4058	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
193	192	csbeq1d 3506	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
194		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (1^st ‘𝑡) = (1^st ‘𝑇))
195	194	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
196	194	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
197	196	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
198	197	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
199	196	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
200	199	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
201	198, 200	uneq12d 3730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
202	195, 201	oveq12d 6567	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
203	202	csbeq2dv 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
204	193, 203	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
205	204	mpteq2dv 4673	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
206	205	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
207	206, 5	elrab2 3333	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
208	207	simprbi 479	. . . . . . . . . . 11 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
209	3, 208	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
210		poimirlem11.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘𝑇) = 0)
211		breq12 4588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = (𝑀 − 1) ∧ (2^nd ‘𝑇) = 0) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
212	210, 211	sylan2 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
213	212	ancoms 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
214	213, 95	ifbieq2d 4061	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
215	214, 112	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
216	215	csbeq1d 3506	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
217	115	imaeq2d 5385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
218	217	xpeq1d 5062	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
219	119	imaeq2d 5385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
220	219	xpeq1d 5062	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
221	218, 220	uneq12d 3730	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑀 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
222	221	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑀 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
223	222	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
224	45, 223	csbied 3526	. . . . . . . . . . . 12 ⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
225	224	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
226	216, 225	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
227		ovex 6577	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V
228	227	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
229	209, 226, 102, 228	fvmptd 6197	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
230	229	fveq1d 6105	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
231	230	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
232	20	sselda 3568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
233		xp1st 7089	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
234	9, 233	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
235		elmapfn 7766	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
236	234, 235	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
237	236	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
238		fnconstg 6006	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
239	145, 238	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))
240		fnconstg 6006	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
241	148, 240	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))
242	239, 241	pm3.2i 470	. . . . . . . . . . . 12 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
243		dff1o3 6056	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
244	243	simprbi 479	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
245	15, 244	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
246		imain 5888	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
247	245, 246	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
248	57	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
249		ima0 5400	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
250	248, 249	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
251	247, 250	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
252		fnun 5911	. . . . . . . . . . . 12 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
253	242, 251, 252	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
254		imaundi 5464	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
255	47	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
256		f1ofo 6057	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
257	15, 256	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
258		foima 6033	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
259	257, 258	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
260	255, 259	eqtr3d 2646	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
261	254, 260	syl5eqr 2658	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
262	261	fneq2d 5896	. . . . . . . . . . 11 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
263	253, 262	mpbid 221	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
264	263	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
265	167	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
266		eqidd 2611	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
267		fvun1 6179	. . . . . . . . . . . . 13 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦))
268	239, 241, 267	mp3an12 1406	. . . . . . . . . . . 12 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦))
269	251, 268	sylan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦))
270	145	fvconst2 6374	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
271	270	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
272	269, 271	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
273	272	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
274	237, 264, 265, 265, 169, 266, 273	ofval 6804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
275	232, 274	mpdan 699	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
276	231, 275	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
277	276	adantrr 749	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
278		poimirlem22.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
279	98, 5, 278, 21, 87	poimirlem10 32589	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘_𝑓 − ((1...𝑁) × {1})) = (1^st ‘(1^st ‘𝑈)))
280	98, 5, 278, 3, 210	poimirlem10 32589	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘_𝑓 − ((1...𝑁) × {1})) = (1^st ‘(1^st ‘𝑇)))
281	279, 280	eqtr3d 2646	. . . . . . 7 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) = (1^st ‘(1^st ‘𝑇)))
282	281	fveq1d 6105	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
283	282	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
284	189, 277, 283	3eqtr3d 2652	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
285		elmapi 7765	. . . . . . . . . . . 12 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
286	234, 285	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
287	286	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾))
288		elfzonn0 12380	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
289	287, 288	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
290	289	nn0red 11229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℝ)
291	290	ltp1d 10833	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) < (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
292	290, 291	gtned 10051	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
293	232, 292	syldan 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
294	293	neneqd 2787	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
295	294	adantrr 749	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
296	284, 295	pm2.65da 598	. . 3 ⊢ (𝜑 → ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
297		iman 439	. . 3 ⊢ ((𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
298	296, 297	sylibr 223	. 2 ⊢ (𝜑 → (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
299	298	ssrdv 3574	1 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {cab 2596 ≠ wne 2780 {crab 2900 Vcvv 3173 ⦋csb 3499 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 ^◡ccnv 5037 ran crn 5039 “ cima 5041 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 1^st c1st 7057 2^nd c2nd 7058 ↑_𝑚 cmap 7744 ℂcc 9813 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ...cfz 12197 ..^cfzo 12334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335

This theorem is referenced by: poimirlem13 32592

W3C validator