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 38136

Description: Lemma for poimir 38157 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 3916	. . . . . . 7 ⊢ (𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
2		imassrn 6062	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ran (2^nd ‘(1^st ‘𝑇))
3		poimirlem12.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
4		elrabi 3648	. . . . . . . . . . . . . . . . 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 2882	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7		xp1st 8004	. . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9		xp2nd 8005	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10	8, 9	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11		fvex 6882	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6796	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3640	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 220	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		f1of 6808	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
16		frn 6701	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
17	14, 15, 16	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑇)) ⊆ (1...𝑁))
18	2, 17	sstrid 3949	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
19		poimirlem12.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
20		elrabi 3648	. . . . . . . . . . . . . . . 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 2882	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
22		xp1st 8004	. . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
24		xp2nd 8005	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
26		fvex 6882	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
27		f1oeq1 6796	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
28	26, 27	elab 3640	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
29	25, 28	sylib 220	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
30		f1ofo 6816	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
31		foima 6785	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
32	29, 30, 31	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = (1...𝑁))
33	18, 32	sseqtrrd 3975	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)))
34	33	ssdifd 4100	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
35		dff1o3 6815	. . . . . . . . . . . 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 501	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
37		imadif 6607	. . . . . . . . . . 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 18	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
39		difun2 4437	. . . . . . . . . . . 12 ⊢ ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
40		poimirlem12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
41		elfznn0 13627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ∈ ℕ₀)
42		nn0p1nn 12522	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
43	40, 41, 42	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
44		nnuz 12880	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
45	43, 44	eleqtrdi 2874	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
46		poimir.0	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
47	46	nncnd 12228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
48		npcan1 11614	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
49	47, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
50		elfzuz3 13528	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
51		peano2uz 12904	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
52	40, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
53	49, 52	eqeltrrd 2865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
54		fzsplit2 13556	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
55	45, 53, 54	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
56		uncom 4113	. . . . . . . . . . . . . 14 ⊢ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
57	55, 56	eqtrdi 2815	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
58	57	difeq1d 4081	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
59		incom 4163	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
60	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
61	60	nn0red 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
62	61	ltp1d 12124	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
63		fzdisj 13558	. . . . . . . . . . . . . . 15 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
64	62, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
65	59, 64	eqtrid 2811	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
66		disj3 4410	. . . . . . . . . . . . 13 ⊢ ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
67	65, 66	sylib 220	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
68	39, 58, 67	3eqtr4a 2825	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
69	68	imaeq2d 6051	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
70	38, 69	eqtr3d 2801	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
71	34, 70	sseqtrd 3974	. . . . . . . 8 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
72	71	sselda 3938	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
73	1, 72	sylan2br 604	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
74		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (2^nd ‘𝑡) = (2^nd ‘𝑈))
75	74	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑈)))
76	75	ifbid 4506	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)))
77	76	csbeq1d 3858	. . . . . . . . . . . . . . . 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 6874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑈)))
79		2fveq3 6874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑈 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑈)))
80	79	imaeq1d 6050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)))
81	80	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}))
82	79	imaeq1d 6050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)))
83	82	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
84	81, 83	uneq12d 4124	. . . . . . . . . . . . . . . . . 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 7416	. . . . . . . . . . . . . . . . 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 3861	. . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . 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 5196	. . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . 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 3656	. . . . . . . . . . . 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 501	. . . . . . . . . . 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 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})))))
93		breq1 5105	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑦 < (2^nd ‘𝑈) ↔ 𝑀 < (2^nd ‘𝑈)))
94		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
95	93, 94	ifbieq1d 4507	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)))
96	46	nnred 12227	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
97		peano2rem 11500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
98	96, 97	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
99		elfzle2 13535	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1))
100	40, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ (𝑁 − 1))
101	96	ltm1d 12126	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
102	61, 98, 96, 100, 101	lelttrd 11343	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < 𝑁)
103		poimirlem12.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑈) = 𝑁)
104	102, 103	breqtrrd 5130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑈))
105	104	iftrued 4490	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)) = 𝑀)
106	95, 105	sylan9eqr 2821	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
107	106	csbeq1d 3858	. . . . . . . . . . 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 7406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
109	108	imaeq2d 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
110	109	xpeq1d 5678	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}))
111		oveq1 7405	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
112	111	oveq1d 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
113	112	imaeq2d 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
114	113	xpeq1d 5678	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
115	110, 114	uneq12d 4124	. . . . . . . . . . . . . . 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 7414	. . . . . . . . . . . . . 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 485	. . . . . . . . . . . . 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 3890	. . . . . . . . . . . 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 484	. . . . . . . . . . 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 2799	. . . . . . . . . 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 7433	. . . . . . . . . 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 6985	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
123	122	fveq1d 6871	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
124	123	adantr 484	. . . . . . 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 6062	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2^nd ‘(1^st ‘𝑈))
126		f1of 6808	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
127		frn 6701	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
128	29, 126, 127	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran (2^nd ‘(1^st ‘𝑈)) ⊆ (1...𝑁))
129	125, 128	sstrid 3949	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
130	129	sselda 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
131		xp1st 8004	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
132		elmapfn 8848	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
133	23, 131, 132	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
134	133	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
135		1ex 11178	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
136		fnconstg 6754	. . . . . . . . . . . . . 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 11175	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
139		fnconstg 6754	. . . . . . . . . . . . . 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 474	. . . . . . . . . . . 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 6608	. . . . . . . . . . . . . 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 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))))
144	64	imaeq2d 6051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑈)) “ ∅))
145		ima0 6068	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ∅) = ∅
146	144, 145	eqtrdi 2815	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
147	143, 146	eqtr3d 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
148		fnun 6637	. . . . . . . . . . . 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 596	. . . . . . . . . . 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 6136	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
151	55	imaeq2d 6051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
152	151, 32	eqtr3d 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
153	150, 152	eqtr3id 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
154	153	fneq2d 6617	. . . . . . . . . . 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 234	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156	155	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
157		ovexd 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
158		inidm 4180	. . . . . . . . 9 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
159		eqidd 2765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
160		fvun2 6961	. . . . . . . . . . . . 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 1474	. . . . . . . . . . . 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 589	. . . . . . . . . . 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 7190	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
164	163	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
165	162, 164	eqtrd 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
166	165	adantr 484	. . . . . . . . 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 7673	. . . . . . . 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 697	. . . . . . 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 8832	. . . . . . . . . . . . 13 ⊢ ((1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
170	23, 131, 169	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)):(1...𝑁)⟶(0..^𝐾))
171	170	ffvelcdmda 7067	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾))
172		elfzonn0 13715	. . . . . . . . . . 11 ⊢ (((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
173	171, 172	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
174	173	nn0cnd 12546	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
175	174	addridd 11385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
176	130, 175	syldan 600	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
177	124, 168, 176	3eqtrd 2803	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
178	73, 177	syldan 600	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
179		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
180	179	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
181	180	ifbid 4506	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
182	181	csbeq1d 3858	. . . . . . . . . . . . . . . 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 6874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
184		2fveq3 6874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
185	184	imaeq1d 6050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
186	185	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
187	184	imaeq1d 6050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
188	187	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
189	186, 188	uneq12d 4124	. . . . . . . . . . . . . . . . . 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 7416	. . . . . . . . . . . . . . . . 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 3861	. . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . 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 5196	. . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . 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 3656	. . . . . . . . . . . 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 501	. . . . . . . . . . 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 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})))))
198		breq1 5105	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑦 < (2^nd ‘𝑇) ↔ 𝑀 < (2^nd ‘𝑇)))
199	198, 94	ifbieq1d 4507	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^nd ‘𝑇), 𝑀, (𝑦 + 1)))
200		poimirlem12.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑇) = 𝑁)
201	102, 200	breqtrrd 5130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑇))
202	201	iftrued 4490	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑇), 𝑀, (𝑦 + 1)) = 𝑀)
203	199, 202	sylan9eqr 2821	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
204	203	csbeq1d 3858	. . . . . . . . . . 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 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
206	205	xpeq1d 5678	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
207	112	imaeq2d 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
208	207	xpeq1d 5678	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
209	206, 208	uneq12d 4124	. . . . . . . . . . . . . . 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 7414	. . . . . . . . . . . . . 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 485	. . . . . . . . . . . . 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 3890	. . . . . . . . . . . 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 484	. . . . . . . . . . 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 2799	. . . . . . . . . 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 7433	. . . . . . . . . 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 6985	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217	216	fveq1d 6871	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
218	217	adantr 484	. . . . . . 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 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
220		xp1st 8004	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
221		elmapfn 8848	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
222	8, 220, 221	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
223	222	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
224		fnconstg 6754	. . . . . . . . . . . . . 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 6754	. . . . . . . . . . . . . 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 474	. . . . . . . . . . . 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 6815	. . . . . . . . . . . . . . 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 501	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
231		imain 6608	. . . . . . . . . . . . . 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 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
233	64	imaeq2d 6051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
234		ima0 6068	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
235	233, 234	eqtrdi 2815	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
236	232, 235	eqtr3d 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
237		fnun 6637	. . . . . . . . . . . 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 596	. . . . . . . . . . 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 6136	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
240	55	imaeq2d 6051	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
241		f1ofo 6816	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
242		foima 6785	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
243	14, 241, 242	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
244	240, 243	eqtr3d 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
245	239, 244	eqtr3id 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
246	245	fneq2d 6617	. . . . . . . . . . 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 234	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
248	247	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
249		ovexd 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
250		eqidd 2765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
251		fvun1 6960	. . . . . . . . . . . . 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 1474	. . . . . . . . . . . 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 589	. . . . . . . . . . 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 7190	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
255	254	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
256	253, 255	eqtrd 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
257	256	adantr 484	. . . . . . . . 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 7673	. . . . . . . 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 697	. . . . . . 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 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
261	260	adantrr 727	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
262	46	nngt0d 12264	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑁)
263	262, 103	breqtrrd 5130	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑈))
264	46, 5, 19, 263	poimirlem5 38129	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑈)))
265	262, 200	breqtrrd 5130	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑇))
266	46, 5, 3, 265	poimirlem5 38129	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
267	264, 266	eqtr3d 2801	. . . . . . 7 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) = (1^st ‘(1^st ‘𝑇)))
268	267	fveq1d 6871	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
269	268	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
270	178, 261, 269	3eqtr3d 2807	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
271		elmapi 8832	. . . . . . . . . . . 12 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
272	8, 220, 271	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
273	272	ffvelcdmda 7067	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾))
274		elfzonn0 13715	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
275	273, 274	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
276	275	nn0red 12545	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℝ)
277	276	ltp1d 12124	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) < (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
278	276, 277	gtned 11320	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
279	219, 278	syldan 600	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
280	279	neneqd 2964	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
281	280	adantrr 727	. . . 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 826	. . 3 ⊢ (𝜑 → ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
283		iman 405	. . 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 236	. 2 ⊢ (𝜑 → (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
285	284	ssrdv 3944	1 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1562 ∈ wcel 2144 {cab 2742 ≠ wne 2959 {crab 3416 Vcvv 3456 ⦋csb 3854 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 ifcif 4482 {csn 4584 class class class wbr 5102 ↦ cmpt 5183 × cxp 5647 ^◡ccnv 5648 ran crn 5650 “ cima 5652 Fun wfun 6517 Fn wfn 6518 ⟶wf 6519 –onto→wfo 6521 –1-1-onto→wf1o 6522 ‘cfv 6523 (class class class)co 7398 ∘_f cof 7660 1^st c1st 7970 2^nd c2nd 7971 ↑_m cmap 8810 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 < clt 11218 ≤ cle 11219 − cmin 11416 ℕcn 12212 ℕ₀cn0 12483 ℤ_≥cuz 12841 ...cfz 13514 ..^cfzo 13661

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-of 7662 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-er 8680 df-map 8812 df-en 8930 df-dom 8931 df-sdom 8932 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-nn 12213 df-n0 12484 df-z 12571 df-uz 12842 df-fz 13515 df-fzo 13662

This theorem is referenced by: poimirlem14 38138

W3C validator