poimirlem6

Description: Lemma for poimir establishing, for a face of a simplex defined by a walk along the edges of an N -cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	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 } ) ) ) ) }
	poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem9.2	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
	poimirlem6.3	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) )
Assertion	poimirlem6	⊢ ( 𝜑 → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		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 } ) ) ) ) }
3		poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
4		poimirlem9.2	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
5		poimirlem6.3	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) )
6		elrabi	⊢ ( 𝑇 ∈ { 𝑡 ∈ ( ( ( ( 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 ... 𝑁 ) ) )
7	6 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
8	3 7	syl	⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
9		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
10	8 9	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
11		xp2nd	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
12	10 11	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
13		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ V
14		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
15	13 14	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
16	12 15	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
17		f1of	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
18	16 17	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
19		elfznn	⊢ ( ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2^nd ‘ 𝑇 ) ∈ ℕ )
20	4 19	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℕ )
21	20	nnzd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℤ )
22		peano2zm	⊢ ( ( 2^nd ‘ 𝑇 ) ∈ ℤ → ( ( 2^nd ‘ 𝑇 ) − 1 ) ∈ ℤ )
23	21 22	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) ∈ ℤ )
24	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
25	23	zred	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) ∈ ℝ )
26	20	nnred	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ∈ ℝ )
27	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28	26	lem1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) ≤ ( 2^nd ‘ 𝑇 ) )
29		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ₀ )
30	1 29	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ₀ )
31	30	nn0red	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
32		elfzle2	⊢ ( ( 2^nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2^nd ‘ 𝑇 ) ≤ ( 𝑁 − 1 ) )
33	4 32	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ≤ ( 𝑁 − 1 ) )
34	27	lem1d	⊢ ( 𝜑 → ( 𝑁 − 1 ) ≤ 𝑁 )
35	26 31 27 33 34	letrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) ≤ 𝑁 )
36	25 26 27 28 35	letrd	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) ≤ 𝑁 )
37		eluz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ↔ ( ( ( 2^nd ‘ 𝑇 ) − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2^nd ‘ 𝑇 ) − 1 ) ≤ 𝑁 ) )
38	23 24 36 37	syl3anbrc	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) )
39		fzss2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) → ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
40	38 39	syl	⊢ ( 𝜑 → ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
41	40 5	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑁 ) )
42	18 41	ffvelrnd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) )
43		xp1st	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
44	10 43	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
45		elmapfn	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
46	44 45	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
48		1ex	⊢ 1 ∈ V
49		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) )
50	48 49	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) )
51		c0ex	⊢ 0 ∈ V
52		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
53	51 52	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) )
54	50 53	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
55		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
56	55	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
57	16 56	syl	⊢ ( 𝜑 → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
58		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) )
59	57 58	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) )
60		elfznn	⊢ ( 𝑀 ∈ ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) → 𝑀 ∈ ℕ )
61	5 60	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
62	61	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
63	62	ltm1d	⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
64		fzdisj	⊢ ( ( 𝑀 − 1 ) < 𝑀 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )
65	63 64	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )
66	65	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
67		ima0	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) = ∅
68	66 67	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
69	59 68	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
70		fnun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) )
71	54 69 70	sylancr	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) )
72	61	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
73		npcan1	⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
74	72 73	syl	⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
75		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
76	61 75	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 1 ) )
77	74 76	eqeltrd	⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
78		nnm1nn0	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ₀ )
79	61 78	syl	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℕ₀ )
80	79	nn0zd	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
81		uzid	⊢ ( ( 𝑀 − 1 ) ∈ ℤ → ( 𝑀 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
82	80 81	syl	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
83		peano2uz	⊢ ( ( 𝑀 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
84	82 83	syl	⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
85	74 84	eqeltrrd	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
86		uzss	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) → ( ℤ_≥ ‘ 𝑀 ) ⊆ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
87	85 86	syl	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝑀 ) ⊆ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
88	61	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
89		elfzle2	⊢ ( 𝑀 ∈ ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) → 𝑀 ≤ ( ( 2^nd ‘ 𝑇 ) − 1 ) )
90	5 89	syl	⊢ ( 𝜑 → 𝑀 ≤ ( ( 2^nd ‘ 𝑇 ) − 1 ) )
91	62 25 27 90 36	letrd	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
92		eluz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
93	88 24 91 92	syl3anbrc	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
94	87 93	sseldd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) )
95		fzsplit2	⊢ ( ( ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) )
96	77 94 95	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) )
97	74	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑀 ... 𝑁 ) )
98	97	uneq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) )
99	96 98	eqtrd	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) )
100	99	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) ) )
101		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
102	100 101	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) )
103		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
104	16 103	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
105		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
106	104 105	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
107	102 106	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
108	107	fneq2d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) ↔ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
109	71 108	mpbid	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
110	109	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
111		ovexd	⊢ ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → ( 1 ... 𝑁 ) ∈ V )
112		inidm	⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
113		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) )
114		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
115		fzpred	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
116	93 115	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
117	116	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
118		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
119	16 118	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
120		fnsnfv	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) )
121	119 41 120	syl2anc	⊢ ( 𝜑 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) )
122	121	uneq1d	⊢ ( 𝜑 → ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
123	114 117 122	3eqtr4a	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) = ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
124	123	xpeq1d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) × { 0 } ) )
125		xpundir	⊢ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) × { 0 } ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) )
126	124 125	eqtrdi	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
127	126	uneq2d	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
128		un12	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
129	127 128	eqtrdi	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
130	129	fveq1d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
131	130	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
132		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
133	51 132	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) )
134	50 133	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
135		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
136	57 135	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
137	79	nn0red	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
138		peano2re	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
139	62 138	syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
140	62	ltp1d	⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
141	137 62 139 63 140	lttrd	⊢ ( 𝜑 → ( 𝑀 − 1 ) < ( 𝑀 + 1 ) )
142		fzdisj	⊢ ( ( 𝑀 − 1 ) < ( 𝑀 + 1 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
143	141 142	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
144	143	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
145	144 67	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
146	136 145	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
147		fnun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
148	134 146 147	sylancr	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
149		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
150		imadif	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { 𝑀 } ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ) )
151	57 150	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { 𝑀 } ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ) )
152		fzsplit	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
153	41 152	syl	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
154	153	difeq1d	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑀 } ) = ( ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∖ { 𝑀 } ) )
155		difundir	⊢ ( ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∖ { 𝑀 } ) = ( ( ( 1 ... 𝑀 ) ∖ { 𝑀 } ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ { 𝑀 } ) )
156		fzsplit2	⊢ ( ( ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑀 ∈ ( ℤ_≥ ‘ ( 𝑀 − 1 ) ) ) → ( 1 ... 𝑀 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑀 ) ) )
157	77 85 156	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑀 ) ) )
158	74	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑀 ) = ( 𝑀 ... 𝑀 ) )
159		fzsn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
160	88 159	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
161	158 160	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑀 ) = { 𝑀 } )
162	161	uneq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑀 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) )
163	157 162	eqtrd	⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) )
164	163	difeq1d	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∖ { 𝑀 } ) = ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) ∖ { 𝑀 } ) )
165		difun2	⊢ ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) ∖ { 𝑀 } ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∖ { 𝑀 } )
166	137 62	ltnled	⊢ ( 𝜑 → ( ( 𝑀 − 1 ) < 𝑀 ↔ ¬ 𝑀 ≤ ( 𝑀 − 1 ) ) )
167	63 166	mpbid	⊢ ( 𝜑 → ¬ 𝑀 ≤ ( 𝑀 − 1 ) )
168		elfzle2	⊢ ( 𝑀 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑀 ≤ ( 𝑀 − 1 ) )
169	167 168	nsyl	⊢ ( 𝜑 → ¬ 𝑀 ∈ ( 1 ... ( 𝑀 − 1 ) ) )
170		difsn	⊢ ( ¬ 𝑀 ∈ ( 1 ... ( 𝑀 − 1 ) ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∖ { 𝑀 } ) = ( 1 ... ( 𝑀 − 1 ) ) )
171	169 170	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∖ { 𝑀 } ) = ( 1 ... ( 𝑀 − 1 ) ) )
172	165 171	syl5eq	⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) ∖ { 𝑀 } ) = ( 1 ... ( 𝑀 − 1 ) ) )
173	164 172	eqtrd	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∖ { 𝑀 } ) = ( 1 ... ( 𝑀 − 1 ) ) )
174	62 139	ltnled	⊢ ( 𝜑 → ( 𝑀 < ( 𝑀 + 1 ) ↔ ¬ ( 𝑀 + 1 ) ≤ 𝑀 ) )
175	140 174	mpbid	⊢ ( 𝜑 → ¬ ( 𝑀 + 1 ) ≤ 𝑀 )
176		elfzle1	⊢ ( 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑀 + 1 ) ≤ 𝑀 )
177	175 176	nsyl	⊢ ( 𝜑 → ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
178		difsn	⊢ ( ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )
179	177 178	syl	⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )
180	173 179	uneq12d	⊢ ( 𝜑 → ( ( ( 1 ... 𝑀 ) ∖ { 𝑀 } ) ∪ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∖ { 𝑀 } ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
181	155 180	syl5eq	⊢ ( 𝜑 → ( ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∖ { 𝑀 } ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
182	154 181	eqtrd	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
183	182	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑁 ) ∖ { 𝑀 } ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
184	121	eqcomd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) = { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } )
185	106 184	difeq12d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) ∖ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ) = ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
186	151 183 185	3eqtr3d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
187	149 186	eqtr3id	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
188	187	fneq2d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) )
189	148 188	mpbid	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
190		eldifsn	⊢ ( 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
191	190	biimpri	⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
192	191	ancoms	⊢ ( ( 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
193		disjdif	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) = ∅
194		fnconstg	⊢ ( 0 ∈ V → ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } )
195	51 194	ax-mp	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) }
196		fvun2	⊢ ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) = ∅ ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
197	195 196	mp3an1	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) = ∅ ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
198	193 197	mpanr1	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
199	189 192 198	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
200	199	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 0 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
201	131 200	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
202	47 110 111 111 112 113 201	ofval	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) ) )
203		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
204	48 203	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) )
205	204 133	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
206		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
207	57 206	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
208		fzdisj	⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
209	140 208	syl	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
210	209	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
211	210 67	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
212	207 211	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ )
213		fnun	⊢ ( ( ( ( ( ( 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 ) ... 𝑁 ) ) ) )
214	205 212 213	sylancr	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
215	153	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
216		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
217	215 216	eqtrdi	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
218	217 106	eqtr3d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
219	218	fneq2d	⊢ ( 𝜑 → ( ( ( ( ( 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 ... 𝑁 ) ) )
220	214 219	mpbid	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
221	220	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
222		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) )
223	163	imaeq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ { 𝑀 } ) ) )
224	121	uneq2d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ { 𝑀 } ) ) )
225	222 223 224	3eqtr4a	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) )
226	225	xpeq1d	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) × { 1 } ) )
227		xpundir	⊢ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) )
228	226 227	eqtrdi	⊢ ( 𝜑 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ) )
229	228	uneq1d	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
230		un23	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) )
231	230	equncomi	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
232	229 231	eqtrdi	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
233	232	fveq1d	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
234	233	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
235		fnconstg	⊢ ( 1 ∈ V → ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } )
236	48 235	ax-mp	⊢ ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) }
237		fvun2	⊢ ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) Fn { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) = ∅ ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
238	236 237	mp3an1	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) = ∅ ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
239	193 238	mpanr1	⊢ ( ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ∧ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∖ { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
240	189 192 239	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
241	240	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( { ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) } × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
242	234 241	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) )
243	47 221 111 111 112 113 242	ofval	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 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 ‘ 𝑇 ) ) ‘ 𝑛 ) + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) ) )
244	202 243	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
245	244	an32s	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
246	245	anasss	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
247		fveq2	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑇 ) )
248	247	breq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
249	248	ifbid	⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
250	249	csbeq1d	⊢ ( 𝑡 = 𝑇 → ⦋ 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 } ) ) ) )
251		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
252		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
253	252	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
254	253	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
255	252	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
256	255	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
257	254 256	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
258	251 257	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 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 } ) ) ) )
259	258	csbeq2dv	⊢ ( 𝑡 = 𝑇 → ⦋ 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 } ) ) ) )
260	250 259	eqtrd	⊢ ( 𝑡 = 𝑇 → ⦋ 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 } ) ) ) )
261	260	mpteq2dv	⊢ ( 𝑡 = 𝑇 → ( 𝑦 ∈ ( 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 } ) ) ) ) )
262	261	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐹 = ( 𝑦 ∈ ( 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 } ) ) ) ) ) )
263	262 2	elrab2	⊢ ( 𝑇 ∈ 𝑆 ↔ ( 𝑇 ∈ ( ( ( ( 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 } ) ) ) ) ) )
264	263	simprbi	⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
265	3 264	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
266		breq1	⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝑦 < ( 2^nd ‘ 𝑇 ) ↔ ( 𝑀 − 1 ) < ( 2^nd ‘ 𝑇 ) ) )
267		id	⊢ ( 𝑦 = ( 𝑀 − 1 ) → 𝑦 = ( 𝑀 − 1 ) )
268	266 267	ifbieq1d	⊢ ( 𝑦 = ( 𝑀 − 1 ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑀 − 1 ) < ( 2^nd ‘ 𝑇 ) , ( 𝑀 − 1 ) , ( 𝑦 + 1 ) ) )
269	26	ltm1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) < ( 2^nd ‘ 𝑇 ) )
270	62 25 26 90 269	lelttrd	⊢ ( 𝜑 → 𝑀 < ( 2^nd ‘ 𝑇 ) )
271	137 62 26 63 270	lttrd	⊢ ( 𝜑 → ( 𝑀 − 1 ) < ( 2^nd ‘ 𝑇 ) )
272	271	iftrued	⊢ ( 𝜑 → if ( ( 𝑀 − 1 ) < ( 2^nd ‘ 𝑇 ) , ( 𝑀 − 1 ) , ( 𝑦 + 1 ) ) = ( 𝑀 − 1 ) )
273	268 272	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑀 − 1 ) )
274	273	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑀 − 1 ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
275		oveq2	⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑀 − 1 ) ) )
276	275	imaeq2d	⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) )
277	276	xpeq1d	⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) )
278	277	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) )
279		oveq1	⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
280	279 74	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( 𝑗 + 1 ) = 𝑀 )
281	280	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( 𝑀 ... 𝑁 ) )
282	281	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
283	282	xpeq1d	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) )
284	278 283	uneq12d	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) )
285	284	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 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 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
286	79 285	csbied	⊢ ( 𝜑 → ⦋ ( 𝑀 − 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 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
287	286	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ ( 𝑀 − 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 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
288	274 287	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
289		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
290	62 27 289 91	lesub1dd	⊢ ( 𝜑 → ( 𝑀 − 1 ) ≤ ( 𝑁 − 1 ) )
291		elfz2nn0	⊢ ( ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑀 − 1 ) ∈ ℕ₀ ∧ ( 𝑁 − 1 ) ∈ ℕ₀ ∧ ( 𝑀 − 1 ) ≤ ( 𝑁 − 1 ) ) )
292	79 30 290 291	syl3anbrc	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
293		ovexd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
294	265 288 292 293	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 − 1 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
295	294	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
296	295	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
297		breq1	⊢ ( 𝑦 = 𝑀 → ( 𝑦 < ( 2^nd ‘ 𝑇 ) ↔ 𝑀 < ( 2^nd ‘ 𝑇 ) ) )
298		id	⊢ ( 𝑦 = 𝑀 → 𝑦 = 𝑀 )
299	297 298	ifbieq1d	⊢ ( 𝑦 = 𝑀 → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑀 < ( 2^nd ‘ 𝑇 ) , 𝑀 , ( 𝑦 + 1 ) ) )
300	270	iftrued	⊢ ( 𝜑 → if ( 𝑀 < ( 2^nd ‘ 𝑇 ) , 𝑀 , ( 𝑦 + 1 ) ) = 𝑀 )
301	299 300	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑀 )
302	301	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ 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 } ) ) ) )
303		oveq2	⊢ ( 𝑗 = 𝑀 → ( 1 ... 𝑗 ) = ( 1 ... 𝑀 ) )
304	303	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
305	304	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) )
306		oveq1	⊢ ( 𝑗 = 𝑀 → ( 𝑗 + 1 ) = ( 𝑀 + 1 ) )
307	306	oveq1d	⊢ ( 𝑗 = 𝑀 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑀 + 1 ) ... 𝑁 ) )
308	307	imaeq2d	⊢ ( 𝑗 = 𝑀 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
309	308	xpeq1d	⊢ ( 𝑗 = 𝑀 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) )
310	305 309	uneq12d	⊢ ( 𝑗 = 𝑀 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
311	310	oveq2d	⊢ ( 𝑗 = 𝑀 → ( ( 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 } ) ) ) )
312	311	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝑀 ) → ( ( 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 } ) ) ) )
313	5 312	csbied	⊢ ( 𝜑 → ⦋ 𝑀 / 𝑗 ⦌ ( ( 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 } ) ) ) )
314	313	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ 𝑀 / 𝑗 ⦌ ( ( 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 } ) ) ) )
315	302 314	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ 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 } ) ) ) )
316	30	nn0zd	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
317	26 27 289 35	lesub1dd	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) − 1 ) ≤ ( 𝑁 − 1 ) )
318		eluz2	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ↔ ( ( ( 2^nd ‘ 𝑇 ) − 1 ) ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ ( ( 2^nd ‘ 𝑇 ) − 1 ) ≤ ( 𝑁 − 1 ) ) )
319	23 316 317 318	syl3anbrc	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) )
320		fzss2	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( ( 2^nd ‘ 𝑇 ) − 1 ) ) → ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
321	319 320	syl	⊢ ( 𝜑 → ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
322		fz1ssfz0	⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) )
323	321 322	sstrdi	⊢ ( 𝜑 → ( 1 ... ( ( 2^nd ‘ 𝑇 ) − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) )
324	323 5	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
325		ovexd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
326	265 315 324 325	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
327	326	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
328	327	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
329	246 296 328	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )
330	329	expr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 ≠ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) )
331	330	necon1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) → 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
332		elmapi	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
333	44 332	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
334	333 42	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ( 0 ..^ 𝐾 ) )
335		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ℕ₀ )
336	334 335	syl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ℕ₀ )
337	336	nn0red	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ℝ )
338	337	ltp1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) < ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 1 ) )
339	337 338	ltned	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ≠ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 1 ) )
340	294	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
341		ovexd	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ V )
342		eqidd	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
343		fzss1	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ 1 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
344	76 343	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
345		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
346	93 345	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
347		fnfvima	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
348	119 344 346 347	syl3anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) )
349		fvun2	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ∧ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
350	50 53 349	mp3an12	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
351	69 348 350	syl2anc	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
352	51	fvconst2	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 0 )
353	348 352	syl	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 0 )
354	351 353	eqtrd	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 0 )
355	354	adantr	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 0 )
356	46 109 341 341 112 342 355	ofval	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 0 ) )
357	42 356	mpdan	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 0 ) )
358	336	nn0cnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ∈ ℂ )
359	358	addid1d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
360	340 357 359	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
361	326	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
362		fzss2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝑁 ) )
363	93 362	syl	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝑁 ) )
364		elfz1end	⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( 1 ... 𝑀 ) )
365	61 364	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑀 ) )
366		fnfvima	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝑁 ) ∧ 𝑀 ∈ ( 1 ... 𝑀 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
367	119 363 365 366	syl3anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) )
368		fvun1	⊢ ( ( ( ( ( 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 ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
369	204 133 368	mp3an12	⊢ ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
370	212 367 369	syl2anc	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
371	48	fvconst2	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 1 )
372	367 371	syl	⊢ ( 𝜑 → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 1 )
373	370 372	eqtrd	⊢ ( 𝜑 → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 1 )
374	373	adantr	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = 1 )
375	46 220 341 341 112 342 374	ofval	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 1 ) )
376	42 375	mpdan	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑀 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑀 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 1 ) )
377	361 376	eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) + 1 ) )
378	339 360 377	3netr4d	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
379		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
380		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
381	379 380	neeq12d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) ) )
382	378 381	syl5ibrcom	⊢ ( 𝜑 → ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) )
383	382	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) )
384	331 383	impbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) ) )
385	42 384	riota5	⊢ ( 𝜑 → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem poimirlem6

Proof