poimirlem20

	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 } ) ) ) ) }
	poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
	poimirlem22.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem22.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 )
	poimirlem21.4	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 𝑁 )
Assertion	poimirlem20	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

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		poimirlem22.1	⊢ ( 𝜑 → 𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
4		poimirlem22.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		poimirlem22.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 )
6		poimirlem21.4	⊢ ( 𝜑 → ( 2^nd ‘ 𝑇 ) = 𝑁 )
7		oveq2	⊢ ( 1 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) )
8	7	eleq1d	⊢ ( 1 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) ) )
9		oveq2	⊢ ( 0 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 0 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) )
10	9	eleq1d	⊢ ( 0 = if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 0 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) ) )
11		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
12	11	oveq1d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) )
14		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 ... 𝑁 ) ) )
15	14 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
16	4 15	syl	⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
17		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
18	16 17	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
19		xp1st	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
20	18 19	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
21		elmapi	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
22	20 21	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
23		xp2nd	⊢ ( ( 1^st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
24	18 23	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
25		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ V
26		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
27	25 26	elab	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
28	24 27	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
29		f1of	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
30	28 29	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
31		elfz1end	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
32	1 31	sylib	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
33	30 32	ffvelrnd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) )
34	22 33	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ( 0 ..^ 𝐾 ) )
35		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ₀ )
36	34 35	syl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ₀ )
37		fvex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ V
38		eleq1	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) )
39	38	anbi2d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) ) )
40		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( 𝑝 ‘ 𝑛 ) = ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
41	40	neeq1d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ( 𝑝 ‘ 𝑛 ) ≠ 0 ↔ ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
42	41	rexbidv	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 ↔ ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
43	39 42	imbi12d	⊢ ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ 𝑛 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) ) )
44	37 43 5	vtocl	⊢ ( ( 𝜑 ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 )
45	33 44	mpdan	⊢ ( 𝜑 → ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 )
46		fveq1	⊢ ( 𝑝 = ( ( 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 ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
47	22	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
49		1ex	⊢ 1 ∈ V
50		fnconstg	⊢ ( 1 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
51	49 50	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) )
52		c0ex	⊢ 0 ∈ V
53		fnconstg	⊢ ( 0 ∈ V → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
54	52 53	ax-mp	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) )
55	51 54	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 ) ... 𝑁 ) ) )
56		dff1o3	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ) )
57	56	simprbi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
58	28 57	syl	⊢ ( 𝜑 → Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
59		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) )
60	58 59	syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) )
61		elfznn0	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℕ₀ )
62	61	nn0red	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
63	62	ltp1d	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 < ( 𝑦 + 1 ) )
64		fzdisj	⊢ ( 𝑦 < ( 𝑦 + 1 ) → ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ∅ )
65	63 64	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ∅ )
66	65	imaeq2d	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) )
67		ima0	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ∅ ) = ∅
68	66 67	eqtrdi	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∩ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ∅ )
69	60 68	sylan9req	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∩ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ∅ )
70		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 ) ... 𝑁 ) ) ) )
71	55 69 70	sylancr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) )
72		imaundi	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∪ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
73		nn0p1nn	⊢ ( 𝑦 ∈ ℕ₀ → ( 𝑦 + 1 ) ∈ ℕ )
74		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
75	73 74	eleqtrdi	⊢ ( 𝑦 ∈ ℕ₀ → ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
76	61 75	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
77	76	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
78	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
79		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
80	78 79	syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
81	80	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
82		elfzuz3	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) )
83		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) )
84	82 83	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) )
85	84	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) )
86	81 85	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝑦 ) )
87		fzsplit2	⊢ ( ( ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 𝑦 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑦 ) ∪ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
88	77 86 87	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑦 ) ∪ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
89	88	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∪ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) )
90		f1ofo	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
91		foima	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
92	28 90 91	3syl	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
93	92	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
94	89 93	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 1 ... 𝑦 ) ∪ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
95	72 94	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) ∪ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
96	95	fneq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 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 ... 𝑁 ) ) )
97	71 96	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
98		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
99	98	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) ∈ V )
100		inidm	⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
101		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
102		f1ofn	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
103	28 102	syl	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
104	103	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
105		fzss1	⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
106	76 105	syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
107	106	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
108		eluzp1p1	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ 𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
109		uzss	⊢ ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) → ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ⊆ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
110	82 108 109	3syl	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ⊆ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
111	110	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ⊆ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
112	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
113	112	uzidd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑁 ) )
114	80	fveq2d	⊢ ( 𝜑 → ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ℤ_≥ ‘ 𝑁 ) )
115	113 114	eleqtrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
116	115	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ_≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
117	111 116	sseldd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) )
118		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑦 + 1 ) ) → 𝑁 ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) )
119	117 118	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) )
120		fnfvima	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
121	104 107 119 120	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
122		fvun2	⊢ ( ( ( ( ( 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 ) ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
123	51 54 122	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 ) ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
124	69 121 123	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
125	52	fvconst2	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = 0 )
126	121 125	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = 0 )
127	124 126	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = 0 )
128	127	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = 0 )
129	48 97 99 99 100 101 128	ofval	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 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 ‘ 𝑇 ) ) ‘ 𝑁 ) ) + 0 ) )
130	33 129	mpidan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 ‘ 𝑇 ) ) ‘ 𝑁 ) ) + 0 ) )
131	36	nn0cnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℂ )
132	131	addid1d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
133	132	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) + 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
134	130 133	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
135	46 134	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
136	135	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
137		fveq2	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑇 ) )
138	137	breq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < ( 2^nd ‘ 𝑇 ) ) )
139	138	ifbid	⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
140		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) )
141		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) )
142	141	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
143	142	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
144	141	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
145	144	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
146	143 145	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 } ) ) )
147	140 146	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 } ) ) ) )
148	139 147	csbeq12dv	⊢ ( 𝑡 = 𝑇 → ⦋ 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 } ) ) ) )
149	148	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 } ) ) ) ) )
150	149	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 } ) ) ) ) ) )
151	150 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 } ) ) ) ) ) )
152	151	simprbi	⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
153	4 152	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
154	62	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℝ )
155		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
156	112 155	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
157	156	zred	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
158	157	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
159	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
160	159	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
161		elfzle2	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
162	161	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
163	159	ltm1d	⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
164	163	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
165	154 158 160 162 164	lelttrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < 𝑁 )
166	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2^nd ‘ 𝑇 ) = 𝑁 )
167	165 166	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < ( 2^nd ‘ 𝑇 ) )
168	167	iftrued	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < ( 2^nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
169	168	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 } ) ) ) )
170		vex	⊢ 𝑦 ∈ V
171		oveq2	⊢ ( 𝑗 = 𝑦 → ( 1 ... 𝑗 ) = ( 1 ... 𝑦 ) )
172	171	imaeq2d	⊢ ( 𝑗 = 𝑦 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
173	172	xpeq1d	⊢ ( 𝑗 = 𝑦 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
174		oveq1	⊢ ( 𝑗 = 𝑦 → ( 𝑗 + 1 ) = ( 𝑦 + 1 ) )
175	174	oveq1d	⊢ ( 𝑗 = 𝑦 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
176	175	imaeq2d	⊢ ( 𝑗 = 𝑦 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
177	176	xpeq1d	⊢ ( 𝑗 = 𝑦 → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
178	173 177	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 } ) ) )
179	178	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 } ) ) ) )
180	170 179	csbie	⊢ ⦋ 𝑦 / 𝑗 ⦌ ( ( 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 } ) ) )
181	169 180	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 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 } ) ) ) )
182	181	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ ( 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 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
183	153 182	eqtrd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
184	183	rneqd	⊢ ( 𝜑 → ran 𝐹 = ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
185	184	eleq2d	⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
186		eqid	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
187		ovex	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
188	186 187	elrnmpti	⊢ ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
189	185 188	bitrdi	⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
190	189	biimpa	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑝 = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
191	136 190	r19.29a	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
192	191	neeq1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ↔ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
193	192	biimpd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ran 𝐹 ) → ( ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
194	193	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ran 𝐹 ( 𝑝 ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
195	45 194	mpd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 )
196		elnnne0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ₀ ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ≠ 0 ) )
197	36 195 196	sylanbrc	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ )
198		nnm1nn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ℕ₀ )
199	197 198	syl	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ℕ₀ )
200		elfzo0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) < 𝐾 ) )
201	34 200	sylib	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) < 𝐾 ) )
202	201	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
203	199	nn0red	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ℝ )
204	36	nn0red	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ℝ )
205	202	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
206	204	ltm1d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) < ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) )
207		elfzolt2	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) < 𝐾 )
208	34 207	syl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) < 𝐾 )
209	203 204 205 206 208	lttrd	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) < 𝐾 )
210		elfzo0	⊢ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ( 0 ..^ 𝐾 ) ↔ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) < 𝐾 ) )
211	199 202 209 210	syl3anbrc	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ( 0 ..^ 𝐾 ) )
212	211	adantr	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) − 1 ) ∈ ( 0 ..^ 𝐾 ) )
213	13 212	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) ∈ ( 0 ..^ 𝐾 ) )
214	213	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 1 ) ∈ ( 0 ..^ 𝐾 ) )
215	22	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) )
216		elfzonn0	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ( 0 ..^ 𝐾 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℕ₀ )
217	215 216	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℕ₀ )
218	217	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) ∈ ℂ )
219	218	subid1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 0 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) )
220	219 215	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 0 ) ∈ ( 0 ..^ 𝐾 ) )
221	220	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − 0 ) ∈ ( 0 ..^ 𝐾 ) )
222	8 10 214 221	ifbothda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ∈ ( 0 ..^ 𝐾 ) )
223	222	fmpttd	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
224		ovex	⊢ ( 0 ..^ 𝐾 ) ∈ V
225	224 98	elmap	⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
226	223 225	sylibr	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) )
227		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
228		1z	⊢ 1 ∈ ℤ
229		peano2z	⊢ ( 1 ∈ ℤ → ( 1 + 1 ) ∈ ℤ )
230	228 229	ax-mp	⊢ ( 1 + 1 ) ∈ ℤ
231	112 230	jctil	⊢ ( 𝜑 → ( ( 1 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
232		elfzelz	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑛 ∈ ℤ )
233	232 228	jctir	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) → ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) )
234		fzsubel	⊢ ( ( ( ( 1 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
235	231 233 234	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
236	227 235	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑛 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
237		ax-1cn	⊢ 1 ∈ ℂ
238	237 237	pncan3oi	⊢ ( ( 1 + 1 ) − 1 ) = 1
239	238	oveq1i	⊢ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
240	236 239	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑛 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
241	240	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ( 𝑛 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
242		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
243	156 228	jctil	⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) )
244		elfzelz	⊢ ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
245	244 228	jctir	⊢ ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑦 ∈ ℤ ∧ 1 ∈ ℤ ) )
246		fzaddel	⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑦 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
247	243 245 246	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑦 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) )
248	242 247	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) )
249	80	oveq2d	⊢ ( 𝜑 → ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 1 + 1 ) ... 𝑁 ) )
250	249	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 1 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 1 + 1 ) ... 𝑁 ) )
251	248 250	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( ( 1 + 1 ) ... 𝑁 ) )
252	232	zcnd	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑛 ∈ ℂ )
253	244	zcnd	⊢ ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℂ )
254		subadd2	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑛 − 1 ) = 𝑦 ↔ ( 𝑦 + 1 ) = 𝑛 ) )
255	237 254	mp3an2	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑛 − 1 ) = 𝑦 ↔ ( 𝑦 + 1 ) = 𝑛 ) )
256		eqcom	⊢ ( 𝑦 = ( 𝑛 − 1 ) ↔ ( 𝑛 − 1 ) = 𝑦 )
257		eqcom	⊢ ( 𝑛 = ( 𝑦 + 1 ) ↔ ( 𝑦 + 1 ) = 𝑛 )
258	255 256 257	3bitr4g	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 = ( 𝑛 − 1 ) ↔ 𝑛 = ( 𝑦 + 1 ) ) )
259	252 253 258	syl2anr	⊢ ( ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑦 = ( 𝑛 − 1 ) ↔ 𝑛 = ( 𝑦 + 1 ) ) )
260	259	ralrimiva	⊢ ( 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ∀ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ( 𝑦 = ( 𝑛 − 1 ) ↔ 𝑛 = ( 𝑦 + 1 ) ) )
261	260	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ( 𝑦 = ( 𝑛 − 1 ) ↔ 𝑛 = ( 𝑦 + 1 ) ) )
262		reu6i	⊢ ( ( ( 𝑦 + 1 ) ∈ ( ( 1 + 1 ) ... 𝑁 ) ∧ ∀ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ( 𝑦 = ( 𝑛 − 1 ) ↔ 𝑛 = ( 𝑦 + 1 ) ) ) → ∃! 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) 𝑦 = ( 𝑛 − 1 ) )
263	251 261 262	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ∃! 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) 𝑦 = ( 𝑛 − 1 ) )
264	263	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∃! 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) 𝑦 = ( 𝑛 − 1 ) )
265		eqid	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) = ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) )
266	265	f1ompt	⊢ ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) : ( ( 1 + 1 ) ... 𝑁 ) –1-1-onto→ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( ∀ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ( 𝑛 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∃! 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) 𝑦 = ( 𝑛 − 1 ) ) )
267	241 264 266	sylanbrc	⊢ ( 𝜑 → ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) : ( ( 1 + 1 ) ... 𝑁 ) –1-1-onto→ ( 1 ... ( 𝑁 − 1 ) ) )
268		f1osng	⊢ ( ( 1 ∈ V ∧ 𝑁 ∈ ℕ ) → { ⟨ 1 , 𝑁 ⟩ } : { 1 } –1-1-onto→ { 𝑁 } )
269	49 1 268	sylancr	⊢ ( 𝜑 → { ⟨ 1 , 𝑁 ⟩ } : { 1 } –1-1-onto→ { 𝑁 } )
270	157 159	ltnled	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
271	163 270	mpbid	⊢ ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
272		elfzle2	⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
273	271 272	nsyl	⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
274		disjsn	⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
275	273 274	sylibr	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ )
276		1re	⊢ 1 ∈ ℝ
277	276	ltp1i	⊢ 1 < ( 1 + 1 )
278	230	zrei	⊢ ( 1 + 1 ) ∈ ℝ
279	276 278	ltnlei	⊢ ( 1 < ( 1 + 1 ) ↔ ¬ ( 1 + 1 ) ≤ 1 )
280	277 279	mpbi	⊢ ¬ ( 1 + 1 ) ≤ 1
281		elfzle1	⊢ ( 1 ∈ ( ( 1 + 1 ) ... 𝑁 ) → ( 1 + 1 ) ≤ 1 )
282	280 281	mto	⊢ ¬ 1 ∈ ( ( 1 + 1 ) ... 𝑁 )
283		disjsn	⊢ ( ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
284	282 283	mpbir	⊢ ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅
285		f1oun	⊢ ( ( ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) : ( ( 1 + 1 ) ... 𝑁 ) –1-1-onto→ ( 1 ... ( 𝑁 − 1 ) ) ∧ { ⟨ 1 , 𝑁 ⟩ } : { 1 } –1-1-onto→ { 𝑁 } ) ∧ ( ( ( ( 1 + 1 ) ... 𝑁 ) ∩ { 1 } ) = ∅ ∧ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ) ) → ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) : ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
286	284 285	mpanr1	⊢ ( ( ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) : ( ( 1 + 1 ) ... 𝑁 ) –1-1-onto→ ( 1 ... ( 𝑁 − 1 ) ) ∧ { ⟨ 1 , 𝑁 ⟩ } : { 1 } –1-1-onto→ { 𝑁 } ) ∧ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ ) → ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) : ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
287	267 269 275 286	syl21anc	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) : ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
288		eleq1	⊢ ( 𝑛 = 1 → ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ 1 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) )
289	282 288	mtbiri	⊢ ( 𝑛 = 1 → ¬ 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
290	289	necon2ai	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑛 ≠ 1 )
291		ifnefalse	⊢ ( 𝑛 ≠ 1 → if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) = ( 𝑛 − 1 ) )
292	290 291	syl	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) → if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) = ( 𝑛 − 1 ) )
293	292	mpteq2ia	⊢ ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) )
294	293	uneq1i	⊢ ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) = ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } )
295	49	a1i	⊢ ( 𝜑 → 1 ∈ V )
296	1 74	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 1 ) )
297		fzpred	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 1 ) → ( 1 ... 𝑁 ) = ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
298	296 297	syl	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
299		uncom	⊢ ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) = ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } )
300	298 299	eqtr2di	⊢ ( 𝜑 → ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) = ( 1 ... 𝑁 ) )
301		iftrue	⊢ ( 𝑛 = 1 → if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) = 𝑁 )
302	301	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) = 𝑁 )
303	295 1 300 302	fmptapd	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) )
304	294 303	eqtr3id	⊢ ( 𝜑 → ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) )
305	80 296	eqeltrd	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
306		uzid	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
307		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
308	156 306 307	3syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
309	80 308	eqeltrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) )
310		fzsplit2	⊢ ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ ( 𝑁 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
311	305 309 310	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
312	80	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
313		fzsn	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
314	112 313	syl	⊢ ( 𝜑 → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
315	312 314	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } )
316	315	uneq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
317	311 316	eqtr2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) = ( 1 ... 𝑁 ) )
318	304 300 317	f1oeq123d	⊢ ( 𝜑 → ( ( ( 𝑛 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↦ ( 𝑛 − 1 ) ) ∪ { ⟨ 1 , 𝑁 ⟩ } ) : ( ( ( 1 + 1 ) ... 𝑁 ) ∪ { 1 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
319	287 318	mpbid	⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
320		f1oco	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
321	28 319 320	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
322	98	mptex	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ∈ V
323	25 322	coex	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ∈ V
324		f1oeq1	⊢ ( 𝑓 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
325	323 324	elab	⊢ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
326	321 325	sylibr	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
327	226 326	opelxpd	⊢ ( 𝜑 → ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
328	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
329		0elfz	⊢ ( 𝑁 ∈ ℕ₀ → 0 ∈ ( 0 ... 𝑁 ) )
330	328 329	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
331	327 330	opelxpd	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
332	1 2 3 4 5 6	poimirlem19	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
333		elfzle1	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 0 ≤ 𝑦 )
334		0re	⊢ 0 ∈ ℝ
335		lenlt	⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 ≤ 𝑦 ↔ ¬ 𝑦 < 0 ) )
336	334 62 335	sylancr	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 0 ≤ 𝑦 ↔ ¬ 𝑦 < 0 ) )
337	333 336	mpbid	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ¬ 𝑦 < 0 )
338	337	iffalsed	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
339	338	csbeq1d	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
340		ovex	⊢ ( 𝑦 + 1 ) ∈ V
341		oveq2	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑦 + 1 ) ) )
342	341	imaeq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
343	342	xpeq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
344		oveq1	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
345	344	oveq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
346	345	imaeq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
347	346	xpeq1d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
348	343 347	uneq12d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
349	348	oveq2d	⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
350	340 349	csbie	⊢ ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
351	339 350	eqtrdi	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
352	351	mpteq2ia	⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
353	332 352	eqtr4di	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
354		opex	⊢ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ ∈ V
355	354 52	op2ndd	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 2^nd ‘ 𝑡 ) = 0 )
356	355	breq2d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 𝑦 < ( 2^nd ‘ 𝑡 ) ↔ 𝑦 < 0 ) )
357	356	ifbid	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) )
358	354 52	op1std	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 1^st ‘ 𝑡 ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ )
359	98	mptex	⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∈ V
360	359 323	op1std	⊢ ( ( 1^st ‘ 𝑡 ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) )
361	358 360	syl	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) )
362	359 323	op2ndd	⊢ ( ( 1^st ‘ 𝑡 ) = ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) )
363	358 362	syl	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) )
364	363	imaeq1d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) )
365	364	xpeq1d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
366	363	imaeq1d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
367	366	xpeq1d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
368	365 367	uneq12d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
369	361 368	oveq12d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
370	357 369	csbeq12dv	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ⦋ if ( 𝑦 < ( 2^nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1^st ‘ ( 1^st ‘ 𝑡 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 1^st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
371	370	mpteq2dv	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 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 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
372	371	eqeq2d	⊢ ( 𝑡 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 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 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
373	372 2	elrab2	⊢ ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ∈ 𝑆 ↔ ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 0 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) ∘_f + ( ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
374	331 353 373	sylanbrc	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ∈ 𝑆 )
375	354 52	op2ndd	⊢ ( 𝑇 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 2^nd ‘ 𝑇 ) = 0 )
376	375	eqcoms	⊢ ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ = 𝑇 → ( 2^nd ‘ 𝑇 ) = 0 )
377	1	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
378	377	necomd	⊢ ( 𝜑 → 0 ≠ 𝑁 )
379		neeq1	⊢ ( ( 2^nd ‘ 𝑇 ) = 0 → ( ( 2^nd ‘ 𝑇 ) ≠ 𝑁 ↔ 0 ≠ 𝑁 ) )
380	378 379	syl5ibrcom	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) = 0 → ( 2^nd ‘ 𝑇 ) ≠ 𝑁 ) )
381	376 380	syl5	⊢ ( 𝜑 → ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ = 𝑇 → ( 2^nd ‘ 𝑇 ) ≠ 𝑁 ) )
382	381	necon2d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑇 ) = 𝑁 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ≠ 𝑇 ) )
383	6 382	mpd	⊢ ( 𝜑 → ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ≠ 𝑇 )
384		neeq1	⊢ ( 𝑧 = ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ → ( 𝑧 ≠ 𝑇 ↔ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ≠ 𝑇 ) )
385	384	rspcev	⊢ ( ( ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ∈ 𝑆 ∧ ⟨ ⟨ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑛 ) − if ( 𝑛 = ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ‘ 𝑁 ) , 1 , 0 ) ) ) , ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) ∘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑛 = 1 , 𝑁 , ( 𝑛 − 1 ) ) ) ) ⟩ , 0 ⟩ ≠ 𝑇 ) → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )
386	374 383 385	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 )

Metamath Proof Explorer

Theorem poimirlem20

Proof