poimirlem7

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

Metamath Proof Explorer

Theorem poimirlem7

Proof