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

Metamath Proof Explorer

Theorem poimirlem7

Proof