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 35715

Description: Lemma for poimir 35737 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..^𝐾) ↑_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...𝑁)))
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 3893	. . . . . . 7 ⊢ (𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
2		imassrn 5969	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ran (2^nd ‘(1^st ‘𝑇))
3		poimirlem12.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
4		elrabi 3611	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁)))
5		poimirlem22.s	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = {𝑡 ∈ ((((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}))))}
6	4, 5	eleq2s 2857	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7	3, 6	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
8		xp1st 7836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9	7, 8	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
10		xp2nd 7837	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (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 6769	. . . . . . . . . . . . . . . 16 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
13		f1oeq1 6688	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
14	12, 13	elab 3602	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15	11, 14	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
16		f1of 6700	. . . . . . . . . . . . . 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	17	frnd 6592	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
19	2, 18	sstrid 3928	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
20		poimirlem11.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
21		elrabi 3611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ {𝑡 ∈ ((((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...𝑁)))
22	21, 5	eleq2s 2857	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
23	20, 22	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
24		xp1st 7836	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
26		xp2nd 7837	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
28		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
29		f1oeq1 6688	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
30	28, 29	elab 3602	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
31	27, 30	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
32		f1ofo 6707	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
34		foima 6677	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
36	19, 35	sseqtrrd 3958	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)))
37	36	ssdifd 4071	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
38		dff1o3 6706	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑈))))
39	38	simprbi 496	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
40	31, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
41		imadif 6502	. . . . . . . . . . 11 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
42	40, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
43		difun2 4411	. . . . . . . . . . . 12 ⊢ ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
44		poimirlem11.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
45		fzsplit 13211	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
47		uncom 4083	. . . . . . . . . . . . . 14 ⊢ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
48	46, 47	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
49	48	difeq1d 4052	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
50		incom 4131	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
51		elfznn 13214	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ)
52	44, 51	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ)
53	52	nnred 11918	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
54	53	ltp1d 11835	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
55		fzdisj 13212	. . . . . . . . . . . . . . 15 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
56	54, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
57	50, 56	syl5eq 2791	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
58		disj3 4384	. . . . . . . . . . . . 13 ⊢ ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
59	57, 58	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
60	43, 49, 59	3eqtr4a 2805	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
61	60	imaeq2d 5958	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
62	42, 61	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
63	37, 62	sseqtrd 3957	. . . . . . . 8 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
64	63	sselda 3917	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
65	1, 64	sylan2br 594	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
66		fveq2 6756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (2^nd ‘𝑡) = (2^nd ‘𝑈))
67	66	breq2d 5082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑈)))
68	67	ifbid 4479	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)))
69	68	csbeq1d 3832	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑈 → ⦋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}))))
70		2fveq3 6761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑈)))
71		2fveq3 6761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑈 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑈)))
72	71	imaeq1d 5957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)))
73	72	xpeq1d 5609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}))
74	71	imaeq1d 5957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)))
75	74	xpeq1d 5609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
76	73, 75	uneq12d 4094	. . . . . . . . . . . . . . . . . 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})))
77	70, 76	oveq12d 7273	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → ((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}))))
78	77	csbeq2dv 3835	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑈 → ⦋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}))))
79	69, 78	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑈 → ⦋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}))))
80	79	mpteq2dv 5172	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑈 → (𝑦 ∈ (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})))))
81	80	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑈 → (𝐹 = (𝑦 ∈ (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}))))))
82	81, 5	elrab2 3620	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ∈ ((((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}))))))
83	82	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑈 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
84	20, 83	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
85		poimirlem11.5	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘𝑈) = 0)
86		breq12 5075	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = (𝑀 − 1) ∧ (2^nd ‘𝑈) = 0) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
87	85, 86	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
88	87	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2^nd ‘𝑈) ↔ (𝑀 − 1) < 0))
89		oveq1 7262	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
90	52	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℂ)
91		npcan1 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
92	90, 91	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
93	89, 92	sylan9eqr 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
94	88, 93	ifbieq2d 4482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
95	52	nnzd 12354	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
96		poimir.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
97	96	nnzd 12354	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℤ)
98		elfzm1b 13263	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
99	95, 97, 98	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
100	44, 99	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
101		elfzle1 13188	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) → 0 ≤ (𝑀 − 1))
102	100, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝑀 − 1))
103		0red 10909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
104		nnm1nn0 12204	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ₀)
105	52, 104	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ₀)
106	105	nn0red 12224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
107	103, 106	lenltd 11051	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < 0))
108	102, 107	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ (𝑀 − 1) < 0)
109	108	iffalsed 4467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
110	109	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
111	94, 110	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
112	111	csbeq1d 3832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋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}))))
113		oveq2 7263	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
114	113	imaeq2d 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
115	114	xpeq1d 5609	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}))
116		oveq1 7262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
117	116	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
118	117	imaeq2d 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
119	118	xpeq1d 5609	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
120	115, 119	uneq12d 4094	. . . . . . . . . . . . . . 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})))
121	120	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑀 → ((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}))))
122	121	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((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}))))
123	44, 122	csbied 3866	. . . . . . . . . . . 12 ⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((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}))))
124	123	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 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}))))
125	112, 124	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋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}))))
126		ovexd 7290	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
127	84, 125, 100, 126	fvmptd 6864	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
128	127	fveq1d 6758	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
129	128	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
130		imassrn 5969	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2^nd ‘(1^st ‘𝑈))
131		f1of 6700	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
132	31, 131	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
133	132	frnd 6592	. . . . . . . . . 10 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
134	130, 133	sstrid 3928	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
135	134	sselda 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
136		xp1st 7836	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
137	25, 136	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
138		elmapfn 8611	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
139	137, 138	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
140	139	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
141		1ex 10902	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
142		fnconstg 6646	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
143	141, 142	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))
144		c0ex 10900	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
145		fnconstg 6646	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
146	144, 145	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))
147	143, 146	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)...𝑁)))
148		imain 6503	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
149	40, 148	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
150	56	imaeq2d 5958	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑈)) “ ∅))
151		ima0 5974	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ∅) = ∅
152	150, 151	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
153	149, 152	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
154		fnun 6529	. . . . . . . . . . . 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)...𝑁))))
155	147, 153, 154	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
156		imaundi 6042	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
157	46	imaeq2d 5958	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
158	157, 35	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
159	156, 158	eqtr3id 2793	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
160	159	fneq2d 6511	. . . . . . . . . . 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...𝑁)))
161	155, 160	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
162	161	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
163		ovexd 7290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
164		inidm 4149	. . . . . . . . 9 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
165		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
166		fvun2 6842	. . . . . . . . . . . . 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})‘𝑦))
167	143, 146, 166	mp3an12 1449	. . . . . . . . . . . 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})‘𝑦))
168	153, 167	sylan 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
169	144	fvconst2 7061	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
170	169	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
171	168, 170	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
172	171	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
173	140, 162, 163, 163, 164, 165, 172	ofval 7522	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0))
174	135, 173	mpdan 683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0))
175		elmapi 8595	. . . . . . . . . . . . 13 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
176	137, 175	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
177	176	ffvelrnda 6943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾))
178		elfzonn0 13360	. . . . . . . . . . 11 ⊢ (((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
179	177, 178	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
180	179	nn0cnd 12225	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
181	135, 180	syldan 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
182	181	addid1d 11105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
183	129, 174, 182	3eqtrd 2782	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
184	65, 183	syldan 590	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
185		fveq2 6756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
186	185	breq2d 5082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
187	186	ifbid 4479	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
188	187	csbeq1d 3832	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ⦋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}))))
189		2fveq3 6761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
190		2fveq3 6761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
191	190	imaeq1d 5957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
192	191	xpeq1d 5609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
193	190	imaeq1d 5957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
194	193	xpeq1d 5609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
195	192, 194	uneq12d 4094	. . . . . . . . . . . . . . . . . 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})))
196	189, 195	oveq12d 7273	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → ((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}))))
197	196	csbeq2dv 3835	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ⦋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}))))
198	188, 197	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → ⦋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}))))
199	198	mpteq2dv 5172	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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})))))
200	199	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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}))))))
201	200, 5	elrab2 3620	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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}))))))
202	201	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
203	3, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
204		poimirlem11.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘𝑇) = 0)
205		breq12 5075	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = (𝑀 − 1) ∧ (2^nd ‘𝑇) = 0) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
206	204, 205	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
207	206	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < 0))
208	207, 93	ifbieq2d 4482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
209	208, 110	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
210	209	csbeq1d 3832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋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}))))
211	113	imaeq2d 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
212	211	xpeq1d 5609	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
213	117	imaeq2d 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
214	213	xpeq1d 5609	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
215	212, 214	uneq12d 4094	. . . . . . . . . . . . . . 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})))
216	215	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑀 → ((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}))))
217	216	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((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}))))
218	44, 217	csbied 3866	. . . . . . . . . . . 12 ⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((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}))))
219	218	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 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}))))
220	210, 219	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋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}))))
221		ovexd 7290	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
222	203, 220, 100, 221	fvmptd 6864	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
223	222	fveq1d 6758	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
224	223	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
225	19	sselda 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
226		xp1st 7836	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
227	9, 226	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
228		elmapfn 8611	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
229	227, 228	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
230	229	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
231		fnconstg 6646	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
232	141, 231	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))
233		fnconstg 6646	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
234	144, 233	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))
235	232, 234	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)...𝑁)))
236		dff1o3 6706	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
237	236	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
238	15, 237	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
239		imain 6503	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
240	238, 239	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
241	56	imaeq2d 5958	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
242		ima0 5974	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
243	241, 242	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
244	240, 243	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
245		fnun 6529	. . . . . . . . . . . 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)...𝑁))))
246	235, 244, 245	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
247		imaundi 6042	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
248	46	imaeq2d 5958	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
249		f1ofo 6707	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
250	15, 249	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
251		foima 6677	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
252	250, 251	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
253	248, 252	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
254	247, 253	eqtr3id 2793	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
255	254	fneq2d 6511	. . . . . . . . . . 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...𝑁)))
256	246, 255	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
257	256	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
258		ovexd 7290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
259		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
260		fvun1 6841	. . . . . . . . . . . . 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})‘𝑦))
261	232, 234, 260	mp3an12 1449	. . . . . . . . . . . 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})‘𝑦))
262	244, 261	sylan 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦))
263	141	fvconst2 7061	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
264	263	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
265	262, 264	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
266	265	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
267	230, 257, 258, 258, 164, 259, 266	ofval 7522	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
268	225, 267	mpdan 683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
269	224, 268	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
270	269	adantrr 713	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
271		poimirlem22.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
272	96, 5, 271, 20, 85	poimirlem10 35714	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘_f − ((1...𝑁) × {1})) = (1^st ‘(1^st ‘𝑈)))
273	96, 5, 271, 3, 204	poimirlem10 35714	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘_f − ((1...𝑁) × {1})) = (1^st ‘(1^st ‘𝑇)))
274	272, 273	eqtr3d 2780	. . . . . . 7 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) = (1^st ‘(1^st ‘𝑇)))
275	274	fveq1d 6758	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
276	275	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
277	184, 270, 276	3eqtr3d 2786	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
278		elmapi 8595	. . . . . . . . . . . 12 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
279	227, 278	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
280	279	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾))
281		elfzonn0 13360	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
282	280, 281	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
283	282	nn0red 12224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℝ)
284	283	ltp1d 11835	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) < (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
285	283, 284	gtned 11040	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
286	225, 285	syldan 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
287	286	neneqd 2947	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
288	287	adantrr 713	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
289	277, 288	pm2.65da 813	. . 3 ⊢ (𝜑 → ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
290		iman 401	. . 3 ⊢ ((𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
291	289, 290	sylibr 233	. 2 ⊢ (𝜑 → (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
292	291	ssrdv 3923	1 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 {cab 2715 ≠ wne 2942 {crab 3067 Vcvv 3422 ⦋csb 3828 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ifcif 4456 {csn 4558 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 ran crn 5581 “ cima 5583 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ∘_f cof 7509 1^st c1st 7802 2^nd c2nd 7803 ↑_m cmap 8573 ℂcc 10800 0cc0 10802 1c1 10803 + caddc 10805 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ...cfz 13168 ..^cfzo 13311

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312

This theorem is referenced by: poimirlem13 35717

W3C validator