Theorem poimirlem8

Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (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 ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
	poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	poimirlem9.2	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
	poimirlem9.3	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion	poimirlem8	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		poimirlem22.s	⊢ 𝑆 = { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) }
3		poimirlem9.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
4		poimirlem9.2	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
5		poimirlem9.3	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		elrabi	⊢ ( 𝑈 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 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	5 7	syl	⊢ ( 𝜑 → 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
9		xp1st	⊢ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
10	8 9	syl	⊢ ( 𝜑 → ( 1st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
11		xp2nd	⊢ ( ( 1st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
12	10 11	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
13		fvex	⊢ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∈ V
14		f1oeq1	⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
15	13 14	elab	⊢ ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
16	12 15	sylib	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
17		f1ofn	⊢ ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
18	16 17	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) )
19		difss	⊢ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⊆ ( 1 ... 𝑁 )
20		fnssres	⊢ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⊆ ( 1 ... 𝑁 ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
21	18 19 20	sylancl	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
22		elrabi	⊢ ( 𝑇 ∈ { 𝑡 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∣ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) } → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
23	22 2	eleq2s	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
24	3 23	syl	⊢ ( 𝜑 → 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
25		xp1st	⊢ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
26	24 25	syl	⊢ ( 𝜑 → ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
27		xp2nd	⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
28	26 27	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
29		fvex	⊢ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ V
30		f1oeq1	⊢ ( 𝑓 = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
31	29 30	elab	⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
32	28 31	sylib	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
33		f1ofn	⊢ ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
34	32 33	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 1st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) )
35		fnssres	⊢ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) Fn ( 1 ... 𝑁 ) ∧ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ⊆ ( 1 ... 𝑁 ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
36	34 19 35	sylancl	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
37		fzp1elp1	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
38	4 37	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
39	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
40		npcan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
41	39 40	syl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
42	41	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
43	38 42	eleqtrd	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) )
44		fzsplit	⊢ ( ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
45	43 44	syl	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
46	45	difeq1d	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
47		difundir	⊢ ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
48		elfznn	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd ‘ 𝑇 ) ∈ ℕ )
49	4 48	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ℕ )
50	49	nncnd	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ℂ )
51		npcan1	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℂ → ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) = ( 2nd ‘ 𝑇 ) )
52	50 51	syl	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) = ( 2nd ‘ 𝑇 ) )
53		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
54	49 53	eleqtrdi	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( ℤ≥ ‘ 1 ) )
55	52 54	eqeltrd	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
56	49	nnzd	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ℤ )
57		peano2zm	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℤ → ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ℤ )
58	56 57	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ℤ )
59		uzid	⊢ ( ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ℤ → ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
60		peano2uz	⊢ ( ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
61	58 59 60	3syl	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
62	52 61	eqeltrrd	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
63		peano2uz	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
64	62 63	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
65		fzsplit2	⊢ ( ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ) )
66	55 64 65	syl2anc	⊢ ( 𝜑 → ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ) )
67	52	oveq1d	⊢ ( 𝜑 → ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = ( ( 2nd ‘ 𝑇 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
68		fzpr	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℤ → ( ( 2nd ‘ 𝑇 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
69	56 68	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
70	67 69	eqtrd	⊢ ( 𝜑 → ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
71	70	uneq2d	⊢ ( 𝜑 → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) − 1 ) + 1 ) ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
72	66 71	eqtrd	⊢ ( 𝜑 → ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
73	72	difeq1d	⊢ ( 𝜑 → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
74	49	nnred	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) ∈ ℝ )
75	74	ltm1d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) − 1 ) < ( 2nd ‘ 𝑇 ) )
76	58	zred	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) − 1 ) ∈ ℝ )
77	76 74	ltnled	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) − 1 ) < ( 2nd ‘ 𝑇 ) ↔ ¬ ( 2nd ‘ 𝑇 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
78	75 77	mpbid	⊢ ( 𝜑 → ¬ ( 2nd ‘ 𝑇 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) )
79		elfzle2	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( 2nd ‘ 𝑇 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) )
80	78 79	nsyl	⊢ ( 𝜑 → ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
81		difsn	⊢ ( ¬ ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
82	80 81	syl	⊢ ( 𝜑 → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
83		peano2re	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ℝ → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ℝ )
84	74 83	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ℝ )
85	74	ltp1d	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) < ( ( 2nd ‘ 𝑇 ) + 1 ) )
86	76 74 84 75 85	lttrd	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) − 1 ) < ( ( 2nd ‘ 𝑇 ) + 1 ) )
87	76 84	ltnled	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) − 1 ) < ( ( 2nd ‘ 𝑇 ) + 1 ) ↔ ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
88	86 87	mpbid	⊢ ( 𝜑 → ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) )
89		elfzle2	⊢ ( ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( ( 2nd ‘ 𝑇 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) − 1 ) )
90	88 89	nsyl	⊢ ( 𝜑 → ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
91		difsn	⊢ ( ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
92	90 91	syl	⊢ ( 𝜑 → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
93	82 92	ineq12d	⊢ ( 𝜑 → ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∩ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) )
94		difun2	⊢ ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
95		df-pr	⊢ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } = ( { ( 2nd ‘ 𝑇 ) } ∪ { ( ( 2nd ‘ 𝑇 ) + 1 ) } )
96	95	difeq2i	⊢ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ ( { ( 2nd ‘ 𝑇 ) } ∪ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
97		difundi	⊢ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ ( { ( 2nd ‘ 𝑇 ) } ∪ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
98	94 96 97	3eqtrri	⊢ ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
99		inidm	⊢ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∩ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) )
100	93 98 99	3eqtr3g	⊢ ( 𝜑 → ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
101	73 100	eqtrd	⊢ ( 𝜑 → ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
102		peano2re	⊢ ( ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ℝ → ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ∈ ℝ )
103	84 102	syl	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ∈ ℝ )
104	84	ltp1d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) + 1 ) < ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) )
105	74 84 103 85 104	lttrd	⊢ ( 𝜑 → ( 2nd ‘ 𝑇 ) < ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) )
106	74 103	ltnled	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑇 ) < ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ↔ ¬ ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( 2nd ‘ 𝑇 ) ) )
107	105 106	mpbid	⊢ ( 𝜑 → ¬ ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( 2nd ‘ 𝑇 ) )
108		elfzle1	⊢ ( ( 2nd ‘ 𝑇 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) → ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( 2nd ‘ 𝑇 ) )
109	107 108	nsyl	⊢ ( 𝜑 → ¬ ( 2nd ‘ 𝑇 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
110		difsn	⊢ ( ¬ ( 2nd ‘ 𝑇 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) → ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
111	109 110	syl	⊢ ( 𝜑 → ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
112	84 103	ltnled	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑇 ) + 1 ) < ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ↔ ¬ ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) + 1 ) ) )
113	104 112	mpbid	⊢ ( 𝜑 → ¬ ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) + 1 ) )
114		elfzle1	⊢ ( ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) → ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ≤ ( ( 2nd ‘ 𝑇 ) + 1 ) )
115	113 114	nsyl	⊢ ( 𝜑 → ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
116		difsn	⊢ ( ¬ ( ( 2nd ‘ 𝑇 ) + 1 ) ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) → ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
117	115 116	syl	⊢ ( 𝜑 → ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
118	111 117	ineq12d	⊢ ( 𝜑 → ( ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∩ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
119	95	difeq2i	⊢ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ ( { ( 2nd ‘ 𝑇 ) } ∪ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
120		difundi	⊢ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ ( { ( 2nd ‘ 𝑇 ) } ∪ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) )
121	119 120	eqtr2i	⊢ ( ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) ∩ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } )
122		inidm	⊢ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∩ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 )
123	118 121 122	3eqtr3g	⊢ ( 𝜑 → ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
124	101 123	uneq12d	⊢ ( 𝜑 → ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ∪ ( ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
125	47 124	eqtrid	⊢ ( 𝜑 → ( ( ( 1 ... ( ( 2nd ‘ 𝑇 ) + 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
126	46 125	eqtrd	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) = ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
127	126	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ↔ 𝑘 ∈ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ) )
128		elun	⊢ ( 𝑘 ∈ ( ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∪ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∨ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
129	127 128	bitrdi	⊢ ( 𝜑 → ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ↔ ( 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∨ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ) )
130	129	biimpa	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∨ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
131		fveq2	⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑇 ) )
132	131	breq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑇 ) ) )
133	132	ifbid	⊢ ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
134	133	csbeq1d	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
135		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑇 ) ) )
136		2fveq3	⊢ ( 𝑡 = 𝑇 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑇 ) ) )
137	136	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
138	137	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
139	136	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
140	139	xpeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
141	138 140	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
142	135 141	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
143	142	csbeq2dv	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
144	134 143	eqtrd	⊢ ( 𝑡 = 𝑇 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
145	144	mpteq2dv	⊢ ( 𝑡 = 𝑇 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
146	145	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
147	146 2	elrab2	⊢ ( 𝑇 ∈ 𝑆 ↔ ( 𝑇 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
148	147	simprbi	⊢ ( 𝑇 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
149	3 148	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
150		xp1st	⊢ ( ( 1st ‘ 𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
151	26 150	syl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
152		elmapi	⊢ ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
153	151 152	syl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
154		elfzoelz	⊢ ( 𝑛 ∈ ( 0 ..^ 𝐾 ) → 𝑛 ∈ ℤ )
155	154	ssriv	⊢ ( 0 ..^ 𝐾 ) ⊆ ℤ
156		fss	⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
157	153 155 156	sylancl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑇 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
158	1 149 157 32 4	poimirlem1	⊢ ( 𝜑 → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) )
159	1	adantr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → 𝑁 ∈ ℕ )
160		fveq2	⊢ ( 𝑡 = 𝑈 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑈 ) )
161	160	breq2d	⊢ ( 𝑡 = 𝑈 → ( 𝑦 < ( 2nd ‘ 𝑡 ) ↔ 𝑦 < ( 2nd ‘ 𝑈 ) ) )
162	161	ifbid	⊢ ( 𝑡 = 𝑈 → if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) )
163	162	csbeq1d	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
164		2fveq3	⊢ ( 𝑡 = 𝑈 → ( 1st ‘ ( 1st ‘ 𝑡 ) ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) )
165		2fveq3	⊢ ( 𝑡 = 𝑈 → ( 2nd ‘ ( 1st ‘ 𝑡 ) ) = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) )
166	165	imaeq1d	⊢ ( 𝑡 = 𝑈 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) )
167	166	xpeq1d	⊢ ( 𝑡 = 𝑈 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
168	165	imaeq1d	⊢ ( 𝑡 = 𝑈 → ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
169	168	xpeq1d	⊢ ( 𝑡 = 𝑈 → ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
170	167 169	uneq12d	⊢ ( 𝑡 = 𝑈 → ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
171	164 170	oveq12d	⊢ ( 𝑡 = 𝑈 → ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
172	171	csbeq2dv	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
173	163 172	eqtrd	⊢ ( 𝑡 = 𝑈 → ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
174	173	mpteq2dv	⊢ ( 𝑡 = 𝑈 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
175	174	eqeq2d	⊢ ( 𝑡 = 𝑈 → ( 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↔ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
176	175 2	elrab2	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
177	176	simprbi	⊢ ( 𝑈 ∈ 𝑆 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
178	5 177	syl	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
179	178	adantr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < ( 2nd ‘ 𝑈 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
180		xp1st	⊢ ( ( 1st ‘ 𝑈 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
181	10 180	syl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
182		elmapi	⊢ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
183	181 182	syl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
184		fss	⊢ ( ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 0 ..^ 𝐾 ) ⊆ ℤ ) → ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
185	183 155 184	sylancl	⊢ ( 𝜑 → ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
186	185	adantr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 1st ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) ⟶ ℤ )
187	16	adantr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ ( 1st ‘ 𝑈 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
188	4	adantr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
189		xp2nd	⊢ ( 𝑈 ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) → ( 2nd ‘ 𝑈 ) ∈ ( 0 ... 𝑁 ) )
190	8 189	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑈 ) ∈ ( 0 ... 𝑁 ) )
191		eldifsn	⊢ ( ( 2nd ‘ 𝑈 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) ↔ ( ( 2nd ‘ 𝑈 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) )
192	191	biimpri	⊢ ( ( ( 2nd ‘ 𝑈 ) ∈ ( 0 ... 𝑁 ) ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑈 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) )
193	190 192	sylan	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ( 2nd ‘ 𝑈 ) ∈ ( ( 0 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) } ) )
194	159 179 186 187 188 193	poimirlem2	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) )
195	194	ex	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑈 ) ≠ ( 2nd ‘ 𝑇 ) → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) ) )
196	195	necon1bd	⊢ ( 𝜑 → ( ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( ( 2nd ‘ 𝑇 ) − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 2nd ‘ 𝑇 ) ) ‘ 𝑛 ) → ( 2nd ‘ 𝑈 ) = ( 2nd ‘ 𝑇 ) ) )
197	158 196	mpd	⊢ ( 𝜑 → ( 2nd ‘ 𝑈 ) = ( 2nd ‘ 𝑇 ) )
198	197	oveq1d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑈 ) − 1 ) = ( ( 2nd ‘ 𝑇 ) − 1 ) )
199	198	oveq2d	⊢ ( 𝜑 → ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) = ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
200	199	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ↔ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) )
201	200	biimpar	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) )
202	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ) → 𝑁 ∈ ℕ )
203	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ) → 𝑈 ∈ 𝑆 )
204	197 4	eqeltrd	⊢ ( 𝜑 → ( 2nd ‘ 𝑈 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
205	204	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ) → ( 2nd ‘ 𝑈 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
206		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ) → 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) )
207	202 2 203 205 206	poimirlem6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑈 ) − 1 ) ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
208	201 207	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
209	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → 𝑁 ∈ ℕ )
210	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → 𝑇 ∈ 𝑆 )
211	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
212		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) )
213	209 2 210 211 212	poimirlem6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
214	208 213	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
215	197	oveq1d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑈 ) + 1 ) = ( ( 2nd ‘ 𝑇 ) + 1 ) )
216	215	oveq1d	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) = ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) )
217	216	oveq1d	⊢ ( 𝜑 → ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) = ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
218	217	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ↔ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) )
219	218	biimpar	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) )
220	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ℕ )
221	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑈 ∈ 𝑆 )
222	204	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( 2nd ‘ 𝑈 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
223		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) )
224	220 2 221 222 223	poimirlem7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑈 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 2 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
225	219 224	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 2 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
226	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ℕ )
227	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑇 ∈ 𝑆 )
228	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( 2nd ‘ 𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
229		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) )
230	226 2 227 228 229	poimirlem7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( ℩ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑘 − 2 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ ( 𝑘 − 1 ) ) ‘ 𝑛 ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
231	225 230	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
232	214 231	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( 2nd ‘ 𝑇 ) − 1 ) ) ∨ 𝑘 ∈ ( ( ( ( 2nd ‘ 𝑇 ) + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
233	130 232	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
234		fvres	⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
235	234	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ‘ 𝑘 ) )
236		fvres	⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
237	236	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ‘ 𝑘 ) )
238	233 235 237	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) → ( ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) = ( ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) ‘ 𝑘 ) )
239	21 36 238	eqfnfvd	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) = ( ( 2nd ‘ ( 1st ‘ 𝑇 ) ) ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd ‘ 𝑇 ) , ( ( 2nd ‘ 𝑇 ) + 1 ) } ) ) )