poimirlem12 - Mathbox for Brendan Leahy

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

Theorem poimirlem12 38368

Description: Lemma for poimir 38389 connecting walks that could yield from a given cube a given face opposite the final 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	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem12.3	⊢ (𝜑 → (2^nd ‘𝑇) = 𝑁)
poimirlem12.4	⊢ (𝜑 → 𝑈 ∈ 𝑆)
poimirlem12.5	⊢ (𝜑 → (2^nd ‘𝑈) = 𝑁)
poimirlem12.6	⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))

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

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

**Proof of Theorem poimirlem12**
Step	Hyp	Ref	Expression
1		eldif 3912	. . . . . . 7 ⊢ (𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
2		imassrn 6071	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ran (2^nd ‘(1^st ‘𝑇))
3		poimirlem12.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
4		elrabi 3644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ {𝑡 ∈ ((((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	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {𝑡 ∈ ((((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 2880	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7		xp1st 8021	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
8	3, 6, 7	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9		xp2nd 8022	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10	8, 9	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11		fvex 6895	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6809	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3636	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		f1of 6821	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
16		frn 6714	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
17	14, 15, 16	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
18	2, 17	sstrid 3945	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
19		poimirlem12.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
20		elrabi 3644	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ {𝑡 ∈ ((((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...𝑁)))
21	20, 5	eleq2s 2880	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
22		xp1st 8021	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
23	19, 21, 22	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
24		xp2nd 8022	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
25	23, 24	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
26		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
27		f1oeq1 6809	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
28	26, 27	elab 3636	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
29	25, 28	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
30		f1ofo 6829	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
31		foima 6798	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
32	29, 30, 31	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
33	18, 32	sseqtrrd 3971	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)))
34	33	ssdifd 4095	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
35		dff1o3 6828	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑈))))
36	35	simprbi 503	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
37		imadif 6621	. . . . . . . . . . 11 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
38	29, 36, 37	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
39		difun2 4440	. . . . . . . . . . . 12 ⊢ ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
40		poimirlem12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
41		elfznn0 13677	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ∈ ℕ₀)
42		nn0p1nn 12570	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
43	40, 41, 42	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
44		nnuz 12929	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
45	43, 44	eleqtrdi 2872	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
46		poimir.0	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
47	46	nncnd 12276	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
48		npcan1 11666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
49	47, 48	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
50		elfzuz3 13577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
51		peano2uz 12953	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
52	40, 50, 51	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
53	49, 52	eqeltrrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
54		fzsplit2 13606	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
55	45, 53, 54	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
56		uncom 4108	. . . . . . . . . . . . . 14 ⊢ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
57	55, 56	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
58	57	difeq1d 4076	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
59		incom 4158	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
60	40, 41	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
61	60	nn0red 12593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
62	61	ltp1d 12172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
63		fzdisj 13608	. . . . . . . . . . . . . . 15 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
64	62, 63	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
65	59, 64	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
66		disj3 4410	. . . . . . . . . . . . 13 ⊢ ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
67	65, 66	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
68	39, 58, 67	3eqtr4a 2823	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
69	68	imaeq2d 6060	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
70	38, 69	eqtr3d 2799	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
71	34, 70	sseqtrd 3970	. . . . . . . 8 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
72	71	sselda 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
73	1, 72	sylan2br 607	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
74		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (2^nd ‘𝑡) = (2^nd ‘𝑈))
75	74	breq2d 5119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑈)))
76	75	ifbid 4509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)))
77	76	csbeq1d 3854	. . . . . . . . . . . . . . . 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}))))
78		2fveq3 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑈)))
79		2fveq3 6887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑈 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑈)))
80	79	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)))
81	80	xpeq1d 5688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}))
82	79	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)))
83	82	xpeq1d 5688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
84	81, 83	uneq12d 4119	. . . . . . . . . . . . . . . . . 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})))
85	78, 84	oveq12d 7434	. . . . . . . . . . . . . . . . 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}))))
86	85	csbeq2dv 3857	. . . . . . . . . . . . . . . 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}))))
87	77, 86	eqtrd 2797	. . . . . . . . . . . . . . 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}))))
88	87	mpteq2dv 5203	. . . . . . . . . . . . . 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})))))
89	88	eqeq2d 2773	. . . . . . . . . . . . 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}))))))
90	89, 5	elrab2 3652	. . . . . . . . . . . 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}))))))
91	90	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑈 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
92	19, 91	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
93		breq1 5110	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑦 < (2^nd ‘𝑈) ↔ 𝑀 < (2^nd ‘𝑈)))
94		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
95	93, 94	ifbieq1d 4510	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)))
96	46	nnred 12275	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
97		peano2rem 11552	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
98	96, 97	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
99		elfzle2 13584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1))
100	40, 99	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ (𝑁 − 1))
101	96	ltm1d 12174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
102	61, 98, 96, 100, 101	lelttrd 11395	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < 𝑁)
103		poimirlem12.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑈) = 𝑁)
104	102, 103	breqtrrd 5137	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑈))
105	104	iftrued 4493	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)) = 𝑀)
106	95, 105	sylan9eqr 2819	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
107	106	csbeq1d 3854	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋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}))))
108		oveq2 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
109	108	imaeq2d 6060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
110	109	xpeq1d 5688	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}))
111		oveq1 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
112	111	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
113	112	imaeq2d 6060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
114	113	xpeq1d 5688	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
115	110, 114	uneq12d 4119	. . . . . . . . . . . . . . 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})))
116	115	oveq2d 7432	. . . . . . . . . . . . . 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}))))
117	116	adantl 487	. . . . . . . . . . . . 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}))))
118	40, 117	csbied 3886	. . . . . . . . . . . 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}))))
119	118	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋𝑀 / 𝑗⦌((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}))))
120	107, 119	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋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}))))
121		ovexd 7451	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
122	92, 120, 40, 121	fvmptd 6998	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
123	122	fveq1d 6884	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
124	123	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
125		imassrn 6071	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2^nd ‘(1^st ‘𝑈))
126		f1of 6821	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
127		frn 6714	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
128	29, 126, 127	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
129	125, 128	sstrid 3945	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
130	129	sselda 3934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
131		xp1st 8021	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
132		elmapfn 8869	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
133	23, 131, 132	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
134	133	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
135		1ex 11230	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
136		fnconstg 6767	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
137	135, 136	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))
138		c0ex 11227	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
139		fnconstg 6767	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
140	138, 139	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))
141	137, 140	pm3.2i 476	. . . . . . . . . . . 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)...𝑁)))
142		imain 6622	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑈)) → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
143	29, 36, 142	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
144	64	imaeq2d 6060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑈)) “ ∅))
145		ima0 6077	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ∅) = ∅
146	144, 145	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
147	143, 146	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
148		fnun 6650	. . . . . . . . . . . 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)...𝑁))))
149	141, 147, 148	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
150		imaundi 6145	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
151	55	imaeq2d 6060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
152	151, 32	eqtr3d 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
153	150, 152	eqtr3id 2811	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
154	153	fneq2d 6630	. . . . . . . . . . 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...𝑁)))
155	149, 154	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156	155	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
157		ovexd 7451	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
158		inidm 4175	. . . . . . . . 9 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
159		eqidd 2763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
160		fvun2 6974	. . . . . . . . . . . . 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})‘𝑦))
161	137, 140, 160	mp3an12 1480	. . . . . . . . . . . 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})‘𝑦))
162	147, 161	sylan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
163	138	fvconst2 7206	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
164	163	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
165	162, 164	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
166	165	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
167	134, 156, 157, 157, 158, 159, 166	ofval 7692	. . . . . . . 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))
168	130, 167	mpdan 700	. . . . . . 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))
169		elmapi 8851	. . . . . . . . . . . . 13 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
170	23, 131, 169	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
171	170	ffvelcdmda 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾))
172		elfzonn0 13765	. . . . . . . . . . 11 ⊢ (((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
173	171, 172	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
174	173	nn0cnd 12594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
175	174	addridd 11437	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
176	130, 175	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
177	124, 168, 176	3eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
178	73, 177	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
179		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
180	179	breq2d 5119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
181	180	ifbid 4509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
182	181	csbeq1d 3854	. . . . . . . . . . . . . . . 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}))))
183		2fveq3 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
184		2fveq3 6887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
185	184	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
186	185	xpeq1d 5688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
187	184	imaeq1d 6059	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
188	187	xpeq1d 5688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
189	186, 188	uneq12d 4119	. . . . . . . . . . . . . . . . . 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})))
190	183, 189	oveq12d 7434	. . . . . . . . . . . . . . . . 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}))))
191	190	csbeq2dv 3857	. . . . . . . . . . . . . . . 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}))))
192	182, 191	eqtrd 2797	. . . . . . . . . . . . . . 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}))))
193	192	mpteq2dv 5203	. . . . . . . . . . . . . 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})))))
194	193	eqeq2d 2773	. . . . . . . . . . . . 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}))))))
195	194, 5	elrab2 3652	. . . . . . . . . . . 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}))))))
196	195	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
197	3, 196	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
198		breq1 5110	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑦 < (2^nd ‘𝑇) ↔ 𝑀 < (2^nd ‘𝑇)))
199	198, 94	ifbieq1d 4510	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^nd ‘𝑇), 𝑀, (𝑦 + 1)))
200		poimirlem12.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑇) = 𝑁)
201	102, 200	breqtrrd 5137	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑇))
202	201	iftrued 4493	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑇), 𝑀, (𝑦 + 1)) = 𝑀)
203	199, 202	sylan9eqr 2819	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
204	203	csbeq1d 3854	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋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}))))
205	108	imaeq2d 6060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
206	205	xpeq1d 5688	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
207	112	imaeq2d 6060	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
208	207	xpeq1d 5688	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
209	206, 208	uneq12d 4119	. . . . . . . . . . . . . . 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})))
210	209	oveq2d 7432	. . . . . . . . . . . . . 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}))))
211	210	adantl 487	. . . . . . . . . . . . 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}))))
212	40, 211	csbied 3886	. . . . . . . . . . . 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}))))
213	212	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋𝑀 / 𝑗⦌((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}))))
214	204, 213	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋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}))))
215		ovexd 7451	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
216	197, 214, 40, 215	fvmptd 6998	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217	216	fveq1d 6884	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
218	217	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
219	18	sselda 3934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
220		xp1st 8021	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
221		elmapfn 8869	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
222	8, 220, 221	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
223	222	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
224		fnconstg 6767	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
225	135, 224	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))
226		fnconstg 6767	. . . . . . . . . . . . . 14 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
227	138, 226	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))
228	225, 227	pm3.2i 476	. . . . . . . . . . . 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)...𝑁)))
229		dff1o3 6828	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
230	229	simprbi 503	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
231		imain 6622	. . . . . . . . . . . . . 14 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
232	14, 230, 231	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
233	64	imaeq2d 6060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
234		ima0 6077	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
235	233, 234	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
236	232, 235	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
237		fnun 6650	. . . . . . . . . . . 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)...𝑁))))
238	228, 236, 237	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
239		imaundi 6145	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
240	55	imaeq2d 6060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
241		f1ofo 6829	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
242		foima 6798	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
243	14, 241, 242	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
244	240, 243	eqtr3d 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
245	239, 244	eqtr3id 2811	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
246	245	fneq2d 6630	. . . . . . . . . . 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...𝑁)))
247	238, 246	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
248	247	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
249		ovexd 7451	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
250		eqidd 2763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
251		fvun1 6973	. . . . . . . . . . . . 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})‘𝑦))
252	225, 227, 251	mp3an12 1480	. . . . . . . . . . . 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})‘𝑦))
253	236, 252	sylan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦))
254	135	fvconst2 7206	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
255	254	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
256	253, 255	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
257	256	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
258	223, 248, 249, 249, 158, 250, 257	ofval 7692	. . . . . . . 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))
259	219, 258	mpdan 700	. . . . . . 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))
260	218, 259	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
261	260	adantrr 730	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
262	46	nngt0d 12312	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑁)
263	262, 103	breqtrrd 5137	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑈))
264	46, 5, 19, 263	poimirlem5 38361	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑈)))
265	262, 200	breqtrrd 5137	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑇))
266	46, 5, 3, 265	poimirlem5 38361	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
267	264, 266	eqtr3d 2799	. . . . . . 7 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) = (1^st ‘(1^st ‘𝑇)))
268	267	fveq1d 6884	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
269	268	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
270	178, 261, 269	3eqtr3d 2805	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
271		elmapi 8851	. . . . . . . . . . . 12 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
272	8, 220, 271	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
273	272	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾))
274		elfzonn0 13765	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
275	273, 274	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
276	275	nn0red 12593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℝ)
277	276	ltp1d 12172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) < (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
278	276, 277	gtned 11372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
279	219, 278	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
280	279	neneqd 2962	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
281	280	adantrr 730	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
282	270, 281	pm2.65da 829	. . 3 ⊢ (𝜑 → ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
283		iman 407	. . 3 ⊢ ((𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
284	282, 283	sylibr 237	. 2 ⊢ (𝜑 → (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
285	284	ssrdv 3940	1 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 {cab 2740 ≠ wne 2957 {crab 3414 Vcvv 3453 ⦋csb 3850 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 ifcif 4485 {csn 4587 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 ^◡ccnv 5658 ran crn 5660 “ cima 5662 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7416 ∘_f cof 7679 1^st c1st 7987 2^nd c2nd 7988 ↑_m cmap 8829 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 < clt 11270 ≤ cle 11271 − cmin 11468 ℕcn 12260 ℕ₀cn0 12531 ℤ_≥cuz 12890 ...cfz 13563 ..^cfzo 13711

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-n0 12532 df-z 12619 df-uz 12891 df-fz 13564 df-fzo 13712

This theorem is used by: poimirlem14 38370

W3C validator