Metamath Proof Explorer


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 syl5eq ( 𝜑 → ( ( ( 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 ) } ) ) )