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 36090

Description: Lemma for poimir 36111 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 3920	. . . . . . 7 ⊢ (𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
2		imassrn 6024	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ran (2^nd ‘(1^st ‘𝑇))
3		poimirlem12.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
4		elrabi 3639	. . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7		xp1st 7953	. . . . . . . . . . . . . . . 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 7954	. . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
12		f1oeq1 6772	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
13	11, 12	elab 3630	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14	10, 13	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15		f1of 6784	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
16		frn 6675	. . . . . . . . . . . . 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 3955	. . . . . . . . . . 11 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
19		poimirlem12.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
20		elrabi 3639	. . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ 𝑆 → 𝑈 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
22		xp1st 7953	. . . . . . . . . . . . . . 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 7954	. . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘(1^st ‘𝑈)) ∈ V
27		f1oeq1 6772	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
28	26, 27	elab 3630	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
29	25, 28	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
30		f1ofo 6791	. . . . . . . . . . . 12 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)–onto→(1...𝑁))
31		foima 6761	. . . . . . . . . . . 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 3985	. . . . . . . . . 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 6790	. . . . . . . . . . . 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 497	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑈)))
37		imadif 6585	. . . . . . . . . . 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 4440	. . . . . . . . . . . 12 ⊢ ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
40		poimirlem12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
41		elfznn0 13534	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ∈ ℕ₀)
42		nn0p1nn 12452	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ)
43	40, 41, 42	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
44		nnuz 12806	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
45	43, 44	eleqtrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
46		poimir.0	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
47	46	nncnd 12169	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
48		npcan1 11580	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
49	47, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
50		elfzuz3 13438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
51		peano2uz 12826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
52	40, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑀))
53	49, 52	eqeltrrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
54		fzsplit2 13466	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
55	45, 53, 54	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
56		uncom 4113	. . . . . . . . . . . . . 14 ⊢ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
57	55, 56	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
58	57	difeq1d 4081	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
59		incom 4161	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
60	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
61	60	nn0red 12474	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
62	61	ltp1d 12085	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
63		fzdisj 13468	. . . . . . . . . . . . . . 15 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
64	62, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
65	59, 64	eqtrid 2788	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
66		disj3 4413	. . . . . . . . . . . . 13 ⊢ ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
67	65, 66	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
68	39, 58, 67	3eqtr4a 2802	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
69	68	imaeq2d 6013	. . . . . . . . . 10 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
70	38, 69	eqtr3d 2778	. . . . . . . . 9 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
71	34, 70	sseqtrd 3984	. . . . . . . 8 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
72	71	sselda 3944	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∖ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
73	1, 72	sylan2br 595	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
74		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (2^nd ‘𝑡) = (2^nd ‘𝑈))
75	74	breq2d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑈)))
76	75	ifbid 4509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑈 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)))
77	76	csbeq1d 3859	. . . . . . . . . . . . . . . 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 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑈 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑈)))
79		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑈 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑈)))
80	79	imaeq1d 6012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)))
81	80	xpeq1d 5662	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑈 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}))
82	79	imaeq1d 6012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑈 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)))
83	82	xpeq1d 5662	. . . . . . . . . . . . . . . . . . 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 7375	. . . . . . . . . . . . . . . . 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 3862	. . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . . 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 5207	. . . . . . . . . . . . . 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 2747	. . . . . . . . . . . . 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 3648	. . . . . . . . . . . 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 497	. . . . . . . . . . 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 5108	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → (𝑦 < (2^nd ‘𝑈) ↔ 𝑀 < (2^nd ‘𝑈)))
94		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀)
95	93, 94	ifbieq1d 4510	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑀 → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)))
96	46	nnred 12168	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
97		peano2rem 11468	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
98	96, 97	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
99		elfzle2 13445	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1))
100	40, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ≤ (𝑁 − 1))
101	96	ltm1d 12087	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
102	61, 98, 96, 100, 101	lelttrd 11313	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 < 𝑁)
103		poimirlem12.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘𝑈) = 𝑁)
104	102, 103	breqtrrd 5133	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑈))
105	104	iftrued 4494	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑈), 𝑀, (𝑦 + 1)) = 𝑀)
106	95, 105	sylan9eqr 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
107	106	csbeq1d 3859	. . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
109	108	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))
110	109	xpeq1d 5662	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}))
111		oveq1 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
112	111	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
113	112	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
114	113	xpeq1d 5662	. . . . . . . . . . . . . . . 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 7373	. . . . . . . . . . . . . 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 482	. . . . . . . . . . . . 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 3893	. . . . . . . . . . . 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 481	. . . . . . . . . . 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 2776	. . . . . . . . . 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 7392	. . . . . . . . . 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 6955	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
123	122	fveq1d 6844	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑈)) ∘_f + ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
124	123	adantr 481	. . . . . . 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 6024	. . . . . . . . . 10 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2^nd ‘(1^st ‘𝑈))
126		f1of 6784	. . . . . . . . . . 11 ⊢ ((2^nd ‘(1^st ‘𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑈)):(1...𝑁)⟶(1...𝑁))
127		frn 6675	. . . . . . . . . . 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 3955	. . . . . . . . 9 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
130	129	sselda 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
131		xp1st 7953	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑈) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑈)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
132		elmapfn 8803	. . . . . . . . . . 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 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1^st ‘(1^st ‘𝑈)) Fn (1...𝑁))
135		1ex 11151	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
136		fnconstg 6730	. . . . . . . . . . . . . 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 11149	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
139		fnconstg 6730	. . . . . . . . . . . . . 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 471	. . . . . . . . . . . 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 6586	. . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑈)) “ ∅))
145		ima0 6029	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ∅) = ∅
146	144, 145	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
147	143, 146	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
148		fnun 6614	. . . . . . . . . . . 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 587	. . . . . . . . . . 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 6102	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)))
151	55	imaeq2d 6013	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
152	151, 32	eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
153	150, 152	eqtr3id 2790	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
154	153	fneq2d 6596	. . . . . . . . . . 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 231	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156	155	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
157		ovexd 7392	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
158		inidm 4178	. . . . . . . . 9 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
159		eqidd 2737	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
160		fvun2 6933	. . . . . . . . . . . . 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 1451	. . . . . . . . . . . 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 580	. . . . . . . . . . 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 7153	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
164	163	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
165	162, 164	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
166	165	adantr 481	. . . . . . . . 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 7628	. . . . . . . 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 685	. . . . . . 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 8787	. . . . . . . . . . . . 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 7035	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾))
172		elfzonn0 13617	. . . . . . . . . . 11 ⊢ (((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
173	171, 172	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℕ₀)
174	173	nn0cnd 12475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑈))‘𝑦) ∈ ℂ)
175	174	addid1d 11355	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
176	130, 175	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1^st ‘(1^st ‘𝑈))‘𝑦) + 0) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
177	124, 168, 176	3eqtrd 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
178	73, 177	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = ((1^st ‘(1^st ‘𝑈))‘𝑦))
179		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
180	179	breq2d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
181	180	ifbid 4509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
182	181	csbeq1d 3859	. . . . . . . . . . . . . . . 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 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
184		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
185	184	imaeq1d 6012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
186	185	xpeq1d 5662	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
187	184	imaeq1d 6012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
188	187	xpeq1d 5662	. . . . . . . . . . . . . . . . . . 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 7375	. . . . . . . . . . . . . . . . 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 3862	. . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . . 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 5207	. . . . . . . . . . . . . 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 2747	. . . . . . . . . . . . 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 3648	. . . . . . . . . . . 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 497	. . . . . . . . . . 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 5108	. . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (2^nd ‘𝑇))
202	201	iftrued 4494	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝑀 < (2^nd ‘𝑇), 𝑀, (𝑦 + 1)) = 𝑀)
203	199, 202	sylan9eqr 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
204	203	csbeq1d 3859	. . . . . . . . . . 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 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
206	205	xpeq1d 5662	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
207	112	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
208	207	xpeq1d 5662	. . . . . . . . . . . . . . . 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 7373	. . . . . . . . . . . . . 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 482	. . . . . . . . . . . . 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 3893	. . . . . . . . . . . 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 481	. . . . . . . . . . 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 2776	. . . . . . . . . 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 7392	. . . . . . . . . 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 6955	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑀) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217	216	fveq1d 6844	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
218	217	adantr 481	. . . . . . 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 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
220		xp1st 7953	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
221		elmapfn 8803	. . . . . . . . . . 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 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
224		fnconstg 6730	. . . . . . . . . . . . . 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 6730	. . . . . . . . . . . . . 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 471	. . . . . . . . . . . 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 6790	. . . . . . . . . . . . . . 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 497	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
231		imain 6586	. . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
234		ima0 6029	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
235	233, 234	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
236	232, 235	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
237		fnun 6614	. . . . . . . . . . . 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 587	. . . . . . . . . . 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 6102	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
240	55	imaeq2d 6013	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
241		f1ofo 6791	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
242		foima 6761	. . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
245	239, 244	eqtr3id 2790	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
246	245	fneq2d 6596	. . . . . . . . . . 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 231	. . . . . . . . . 10 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
248	247	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
249		ovexd 7392	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
250		eqidd 2737	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
251		fvun1 6932	. . . . . . . . . . . . 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 1451	. . . . . . . . . . . 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 580	. . . . . . . . . . 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 7153	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
255	254	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
256	253, 255	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
257	256	adantr 481	. . . . . . . . 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 7628	. . . . . . . 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 685	. . . . . . 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 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
261	260	adantrr 715	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((𝐹‘𝑀)‘𝑦) = (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
262	46	nngt0d 12202	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑁)
263	262, 103	breqtrrd 5133	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑈))
264	46, 5, 19, 263	poimirlem5 36083	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑈)))
265	262, 200	breqtrrd 5133	. . . . . . . . 9 ⊢ (𝜑 → 0 < (2^nd ‘𝑇))
266	46, 5, 3, 265	poimirlem5 36083	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
267	264, 266	eqtr3d 2778	. . . . . . 7 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑈)) = (1^st ‘(1^st ‘𝑇)))
268	267	fveq1d 6844	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
269	268	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → ((1^st ‘(1^st ‘𝑈))‘𝑦) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
270	178, 261, 269	3eqtr3d 2784	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
271		elmapi 8787	. . . . . . . . . . . 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 7035	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾))
274		elfzonn0 13617	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
275	273, 274	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℕ₀)
276	275	nn0red 12474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) ∈ ℝ)
277	276	ltp1d 12085	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑦) < (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1))
278	276, 277	gtned 11290	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
279	219, 278	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) ≠ ((1^st ‘(1^st ‘𝑇))‘𝑦))
280	279	neneqd 2948	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → ¬ (((1^st ‘(1^st ‘𝑇))‘𝑦) + 1) = ((1^st ‘(1^st ‘𝑇))‘𝑦))
281	280	adantrr 715	. . . 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 815	. . 3 ⊢ (𝜑 → ¬ (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
283		iman 402	. . 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 233	. 2 ⊢ (𝜑 → (𝑦 ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀))))
285	284	ssrdv 3950	1 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ⊆ ((2^nd ‘(1^st ‘𝑈)) “ (1...𝑀)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2713 ≠ wne 2943 {crab 3407 Vcvv 3445 ⦋csb 3855 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 {csn 4586 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 ^◡ccnv 5632 ran crn 5634 “ cima 5636 Fun wfun 6490 Fn wfn 6491 ⟶wf 6492 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 1^st c1st 7919 2^nd c2nd 7920 ↑_m cmap 8765 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 ≤ cle 11190 − cmin 11385 ℕcn 12153 ℕ₀cn0 12413 ℤ_≥cuz 12763 ...cfz 13424 ..^cfzo 13567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-n0 12414 df-z 12500 df-uz 12764 df-fz 13425 df-fzo 13568

This theorem is referenced by: poimirlem14 36092

W3C validator