Metamath Proof Explorer


Theorem poimirlem15

Description: Lemma for poimir , that the face in poimirlem22 is a face. (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 } ) ) ) ) }
poimirlem22.1 ( 𝜑𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
poimirlem22.2 ( 𝜑𝑇𝑆 )
poimirlem15.3 ( 𝜑 → ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
Assertion poimirlem15 ( 𝜑 → ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ 𝑆 )

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 poimirlem22.1 ( 𝜑𝐹 : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
4 poimirlem22.2 ( 𝜑𝑇𝑆 )
5 poimirlem15.3 ( 𝜑 → ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
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 4 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 xp1st ( ( 1st𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 1st𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
11 8 9 10 3syl ( 𝜑 → ( 1st ‘ ( 1st𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
12 xp2nd ( ( 1st𝑇 ) ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 1st𝑇 ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
13 8 9 12 3syl ( 𝜑 → ( 2nd ‘ ( 1st𝑇 ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
14 fvex ( 2nd ‘ ( 1st𝑇 ) ) ∈ V
15 f1oeq1 ( 𝑓 = ( 2nd ‘ ( 1st𝑇 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 1st𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
16 14 15 elab ( ( 2nd ‘ ( 1st𝑇 ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 1st𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
17 13 16 sylib ( 𝜑 → ( 2nd ‘ ( 1st𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
18 elfznn ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd𝑇 ) ∈ ℕ )
19 5 18 syl ( 𝜑 → ( 2nd𝑇 ) ∈ ℕ )
20 19 nnred ( 𝜑 → ( 2nd𝑇 ) ∈ ℝ )
21 20 ltp1d ( 𝜑 → ( 2nd𝑇 ) < ( ( 2nd𝑇 ) + 1 ) )
22 20 21 ltned ( 𝜑 → ( 2nd𝑇 ) ≠ ( ( 2nd𝑇 ) + 1 ) )
23 22 necomd ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ≠ ( 2nd𝑇 ) )
24 fvex ( 2nd𝑇 ) ∈ V
25 ovex ( ( 2nd𝑇 ) + 1 ) ∈ V
26 f1oprg ( ( ( ( 2nd𝑇 ) ∈ V ∧ ( ( 2nd𝑇 ) + 1 ) ∈ V ) ∧ ( ( ( 2nd𝑇 ) + 1 ) ∈ V ∧ ( 2nd𝑇 ) ∈ V ) ) → ( ( ( 2nd𝑇 ) ≠ ( ( 2nd𝑇 ) + 1 ) ∧ ( ( 2nd𝑇 ) + 1 ) ≠ ( 2nd𝑇 ) ) → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } ) )
27 24 25 25 24 26 mp4an ( ( ( 2nd𝑇 ) ≠ ( ( 2nd𝑇 ) + 1 ) ∧ ( ( 2nd𝑇 ) + 1 ) ≠ ( 2nd𝑇 ) ) → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } )
28 22 23 27 syl2anc ( 𝜑 → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } )
29 prcom { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) }
30 f1oeq3 ( { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } ↔ { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
31 29 30 ax-mp ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } ↔ { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
32 28 31 sylib ( 𝜑 → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
33 f1oi ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
34 disjdif ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ∅
35 f1oun ( ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∧ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ∧ ( ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ∅ ∧ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ∅ ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) –1-1-onto→ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
36 34 34 35 mpanr12 ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∧ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) : ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) –1-1-onto→ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) –1-1-onto→ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
37 32 33 36 sylancl ( 𝜑 → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) –1-1-onto→ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
38 1 nncnd ( 𝜑𝑁 ∈ ℂ )
39 npcan1 ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
40 38 39 syl ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
41 1 nnzd ( 𝜑𝑁 ∈ ℤ )
42 peano2zm ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
43 41 42 syl ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
44 uzid ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
45 peano2uz ( ( 𝑁 − 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
46 43 44 45 3syl ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
47 40 46 eqeltrrd ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
48 fzss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
49 47 48 syl ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
50 49 5 sseldd ( 𝜑 → ( 2nd𝑇 ) ∈ ( 1 ... 𝑁 ) )
51 19 peano2nnd ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ∈ ℕ )
52 43 zred ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
53 1 nnred ( 𝜑𝑁 ∈ ℝ )
54 elfzle2 ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 2nd𝑇 ) ≤ ( 𝑁 − 1 ) )
55 5 54 syl ( 𝜑 → ( 2nd𝑇 ) ≤ ( 𝑁 − 1 ) )
56 53 ltm1d ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
57 20 52 53 55 56 lelttrd ( 𝜑 → ( 2nd𝑇 ) < 𝑁 )
58 19 nnzd ( 𝜑 → ( 2nd𝑇 ) ∈ ℤ )
59 zltp1le ( ( ( 2nd𝑇 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 2nd𝑇 ) < 𝑁 ↔ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) )
60 58 41 59 syl2anc ( 𝜑 → ( ( 2nd𝑇 ) < 𝑁 ↔ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) )
61 57 60 mpbid ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 )
62 fznn ( 𝑁 ∈ ℤ → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) ) )
63 41 62 syl ( 𝜑 → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) ) )
64 51 61 63 mpbir2and ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) )
65 prssi ( ( ( 2nd𝑇 ) ∈ ( 1 ... 𝑁 ) ∧ ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑁 ) ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) )
66 50 64 65 syl2anc ( 𝜑 → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) )
67 undif ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... 𝑁 ) ↔ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) )
68 66 67 sylib ( 𝜑 → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) )
69 f1oeq23 ( ( ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) ∧ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... 𝑁 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) –1-1-onto→ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ↔ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
70 68 68 69 syl2anc ( 𝜑 → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) –1-1-onto→ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ↔ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
71 37 70 mpbid ( 𝜑 → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
72 f1oco ( ( ( 2nd ‘ ( 1st𝑇 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) → ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
73 17 71 72 syl2anc ( 𝜑 → ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
74 prex { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∈ V
75 ovex ( 1 ... 𝑁 ) ∈ V
76 difexg ( ( 1 ... 𝑁 ) ∈ V → ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∈ V )
77 resiexg ( ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∈ V → ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ∈ V )
78 75 76 77 mp2b ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ∈ V
79 74 78 unex ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ∈ V
80 14 79 coex ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ∈ V
81 f1oeq1 ( 𝑓 = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
82 80 81 elab ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
83 73 82 sylibr ( 𝜑 → ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
84 opelxpi ( ( ( 1st ‘ ( 1st𝑇 ) ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ∧ ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ∈ { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
85 11 83 84 syl2anc ( 𝜑 → ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
86 fz1ssfz0 ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
87 49 86 sstrdi ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
88 87 5 sseldd ( 𝜑 → ( 2nd𝑇 ) ∈ ( 0 ... 𝑁 ) )
89 opelxpi ( ( ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ ( 2nd𝑇 ) ∈ ( 0 ... 𝑁 ) ) → ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
90 85 88 89 syl2anc ( 𝜑 → ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) )
91 fveq2 ( 𝑡 = 𝑇 → ( 2nd𝑡 ) = ( 2nd𝑇 ) )
92 91 breq2d ( 𝑡 = 𝑇 → ( 𝑦 < ( 2nd𝑡 ) ↔ 𝑦 < ( 2nd𝑇 ) ) )
93 92 ifbid ( 𝑡 = 𝑇 → if ( 𝑦 < ( 2nd𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
94 93 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 } ) ) ) )
95 2fveq3 ( 𝑡 = 𝑇 → ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
96 2fveq3 ( 𝑡 = 𝑇 → ( 2nd ‘ ( 1st𝑡 ) ) = ( 2nd ‘ ( 1st𝑇 ) ) )
97 96 imaeq1d ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) )
98 97 xpeq1d ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
99 96 imaeq1d ( 𝑡 = 𝑇 → ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
100 99 xpeq1d ( 𝑡 = 𝑇 → ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
101 98 100 uneq12d ( 𝑡 = 𝑇 → ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
102 95 101 oveq12d ( 𝑡 = 𝑇 → ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
103 102 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 } ) ) ) )
104 94 103 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 } ) ) ) )
105 104 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 } ) ) ) ) )
106 105 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 } ) ) ) ) ) )
107 106 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 } ) ) ) ) ) )
108 107 simprbi ( 𝑇𝑆𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
109 4 108 syl ( 𝜑𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
110 imaco ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... 𝑦 ) ) )
111 f1ofn ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
112 28 111 syl ( 𝜑 → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
113 112 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
114 incom ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( 1 ... 𝑦 ) ) = ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
115 elfznn0 ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℕ0 )
116 115 nn0red ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
117 ltnle ( ( 𝑦 ∈ ℝ ∧ ( 2nd𝑇 ) ∈ ℝ ) → ( 𝑦 < ( 2nd𝑇 ) ↔ ¬ ( 2nd𝑇 ) ≤ 𝑦 ) )
118 116 20 117 syl2anr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 < ( 2nd𝑇 ) ↔ ¬ ( 2nd𝑇 ) ≤ 𝑦 ) )
119 118 biimpa ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ¬ ( 2nd𝑇 ) ≤ 𝑦 )
120 elfzle2 ( ( 2nd𝑇 ) ∈ ( 1 ... 𝑦 ) → ( 2nd𝑇 ) ≤ 𝑦 )
121 119 120 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ¬ ( 2nd𝑇 ) ∈ ( 1 ... 𝑦 ) )
122 disjsn ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) } ) = ∅ ↔ ¬ ( 2nd𝑇 ) ∈ ( 1 ... 𝑦 ) )
123 121 122 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) } ) = ∅ )
124 116 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → 𝑦 ∈ ℝ )
125 20 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) ∈ ℝ )
126 51 nnred ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ∈ ℝ )
127 126 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℝ )
128 simpr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → 𝑦 < ( 2nd𝑇 ) )
129 21 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) < ( ( 2nd𝑇 ) + 1 ) )
130 124 125 127 128 129 lttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → 𝑦 < ( ( 2nd𝑇 ) + 1 ) )
131 ltnle ( ( 𝑦 ∈ ℝ ∧ ( ( 2nd𝑇 ) + 1 ) ∈ ℝ ) → ( 𝑦 < ( ( 2nd𝑇 ) + 1 ) ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑦 ) )
132 116 126 131 syl2anr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 < ( ( 2nd𝑇 ) + 1 ) ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑦 ) )
133 132 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 𝑦 < ( ( 2nd𝑇 ) + 1 ) ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑦 ) )
134 130 133 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ¬ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑦 )
135 elfzle2 ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ≤ 𝑦 )
136 134 135 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑦 ) )
137 disjsn ( ( ( 1 ... 𝑦 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... 𝑦 ) )
138 136 137 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 1 ... 𝑦 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
139 123 138 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( 1 ... 𝑦 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ∅ ∪ ∅ ) )
140 df-pr { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } = ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } )
141 140 ineq2i ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ( 1 ... 𝑦 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) )
142 indi ( ( 1 ... 𝑦 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( 1 ... 𝑦 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) )
143 141 142 eqtr2i ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( 1 ... 𝑦 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
144 un0 ( ∅ ∪ ∅ ) = ∅
145 139 143 144 3eqtr3g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
146 114 145 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( 1 ... 𝑦 ) ) = ∅ )
147 fnimadisj ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∧ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( 1 ... 𝑦 ) ) = ∅ ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... 𝑦 ) ) = ∅ )
148 113 146 147 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... 𝑦 ) ) = ∅ )
149 40 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
150 elfzuz3 ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ𝑦 ) )
151 peano2uz ( ( 𝑁 − 1 ) ∈ ( ℤ𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑦 ) )
152 150 151 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑦 ) )
153 152 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑦 ) )
154 149 153 eqeltrrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ𝑦 ) )
155 fzss2 ( 𝑁 ∈ ( ℤ𝑦 ) → ( 1 ... 𝑦 ) ⊆ ( 1 ... 𝑁 ) )
156 reldisj ( ( 1 ... 𝑦 ) ⊆ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( 1 ... 𝑦 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
157 154 155 156 3syl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( 1 ... 𝑦 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
158 157 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 1 ... 𝑦 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( 1 ... 𝑦 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
159 145 158 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 1 ... 𝑦 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
160 resiima ( ( 1 ... 𝑦 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... 𝑦 ) ) = ( 1 ... 𝑦 ) )
161 159 160 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... 𝑦 ) ) = ( 1 ... 𝑦 ) )
162 148 161 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... 𝑦 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... 𝑦 ) ) ) = ( ∅ ∪ ( 1 ... 𝑦 ) ) )
163 imaundir ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... 𝑦 ) ) = ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... 𝑦 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... 𝑦 ) ) )
164 uncom ( ∅ ∪ ( 1 ... 𝑦 ) ) = ( ( 1 ... 𝑦 ) ∪ ∅ )
165 un0 ( ( 1 ... 𝑦 ) ∪ ∅ ) = ( 1 ... 𝑦 )
166 164 165 eqtr2i ( 1 ... 𝑦 ) = ( ∅ ∪ ( 1 ... 𝑦 ) )
167 162 163 166 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... 𝑦 ) ) = ( 1 ... 𝑦 ) )
168 167 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... 𝑦 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
169 110 168 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
170 169 xpeq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
171 imaco ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
172 imaundir ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
173 imassrn ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ }
174 173 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
175 fnima ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
176 28 111 175 3syl ( 𝜑 → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
177 176 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
178 elfzelz ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
179 zltp1le ( ( 𝑦 ∈ ℤ ∧ ( 2nd𝑇 ) ∈ ℤ ) → ( 𝑦 < ( 2nd𝑇 ) ↔ ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) ) )
180 178 58 179 syl2anr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 < ( 2nd𝑇 ) ↔ ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) ) )
181 180 biimpa ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) )
182 20 53 57 ltled ( 𝜑 → ( 2nd𝑇 ) ≤ 𝑁 )
183 182 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) ≤ 𝑁 )
184 58 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2nd𝑇 ) ∈ ℤ )
185 nn0p1nn ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ )
186 115 185 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℕ )
187 186 nnzd ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℤ )
188 187 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ℤ )
189 41 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
190 elfz ( ( ( 2nd𝑇 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 2nd𝑇 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) ∧ ( 2nd𝑇 ) ≤ 𝑁 ) ) )
191 184 188 189 190 syl3anc ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) ∧ ( 2nd𝑇 ) ≤ 𝑁 ) ) )
192 191 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd𝑇 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( 2nd𝑇 ) ∧ ( 2nd𝑇 ) ≤ 𝑁 ) ) )
193 181 183 192 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) )
194 1red ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → 1 ∈ ℝ )
195 ltle ( ( 𝑦 ∈ ℝ ∧ ( 2nd𝑇 ) ∈ ℝ ) → ( 𝑦 < ( 2nd𝑇 ) → 𝑦 ≤ ( 2nd𝑇 ) ) )
196 116 20 195 syl2anr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 < ( 2nd𝑇 ) → 𝑦 ≤ ( 2nd𝑇 ) ) )
197 196 imp ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → 𝑦 ≤ ( 2nd𝑇 ) )
198 124 125 194 197 leadd1dd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( 𝑦 + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) )
199 61 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 )
200 58 peano2zd ( 𝜑 → ( ( 2nd𝑇 ) + 1 ) ∈ ℤ )
201 200 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℤ )
202 elfz ( ( ( ( 2nd𝑇 ) + 1 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ∧ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) ) )
203 201 188 189 202 syl3anc ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ∧ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) ) )
204 203 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( ( 𝑦 + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ∧ ( ( 2nd𝑇 ) + 1 ) ≤ 𝑁 ) ) )
205 198 199 204 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd𝑇 ) + 1 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) )
206 prssi ( ( ( 2nd𝑇 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ∧ ( ( 2nd𝑇 ) + 1 ) ∈ ( ( 𝑦 + 1 ) ... 𝑁 ) ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( ( 𝑦 + 1 ) ... 𝑁 ) )
207 193 205 206 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( ( 𝑦 + 1 ) ... 𝑁 ) )
208 imass2 ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( ( 𝑦 + 1 ) ... 𝑁 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
209 207 208 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
210 177 209 eqsstrrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
211 174 210 eqssd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
212 f1ofo ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –1-1-onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } )
213 forn ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } : { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } –onto→ { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } )
214 28 212 213 3syl ( 𝜑 → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) } )
215 214 29 eqtrdi ( 𝜑 → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
216 215 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
217 211 216 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
218 undif ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( ( 𝑦 + 1 ) ... 𝑁 ) ↔ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
219 207 218 sylib ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
220 219 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
221 fnresi ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
222 incom ( ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
223 222 34 eqtri ( ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅
224 fnimadisj ( ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∧ ( ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
225 221 223 224 mp2an ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅
226 225 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
227 nnuz ℕ = ( ℤ ‘ 1 )
228 186 227 eleqtrdi ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( ℤ ‘ 1 ) )
229 fzss1 ( ( 𝑦 + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
230 228 229 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
231 230 ssdifd ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
232 resiima ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
233 231 232 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
234 233 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
235 226 234 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
236 imaundi ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
237 uncom ( ∅ ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ )
238 un0 ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
239 237 238 eqtr2i ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
240 235 236 239 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
241 220 240 eqtr3d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
242 217 241 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
243 172 242 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
244 243 219 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
245 244 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
246 171 245 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
247 246 xpeq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
248 170 247 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
249 248 oveq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
250 iftrue ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
251 250 csbeq1d ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = 𝑦 / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
252 vex 𝑦 ∈ V
253 oveq2 ( 𝑗 = 𝑦 → ( 1 ... 𝑗 ) = ( 1 ... 𝑦 ) )
254 253 imaeq2d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) )
255 254 xpeq1d ( 𝑗 = 𝑦 → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
256 oveq1 ( 𝑗 = 𝑦 → ( 𝑗 + 1 ) = ( 𝑦 + 1 ) )
257 256 oveq1d ( 𝑗 = 𝑦 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
258 257 imaeq2d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
259 258 xpeq1d ( 𝑗 = 𝑦 → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
260 255 259 uneq12d ( 𝑗 = 𝑦 → ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
261 260 oveq2d ( 𝑗 = 𝑦 → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
262 252 261 csbie 𝑦 / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
263 251 262 eqtrdi ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
264 263 adantl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
265 250 csbeq1d ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = 𝑦 / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
266 253 imaeq2d ( 𝑗 = 𝑦 → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
267 266 xpeq1d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
268 257 imaeq2d ( 𝑗 = 𝑦 → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
269 268 xpeq1d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
270 267 269 uneq12d ( 𝑗 = 𝑦 → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
271 270 oveq2d ( 𝑗 = 𝑦 → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
272 252 271 csbie 𝑦 / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
273 265 272 eqtrdi ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
274 273 adantl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
275 249 264 274 3eqtr4d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
276 lenlt ( ( ( 2nd𝑇 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 2nd𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2nd𝑇 ) ) )
277 20 116 276 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2nd𝑇 ) ) )
278 277 biimpar ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) ≤ 𝑦 )
279 imaco ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
280 imaundir ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
281 imassrn ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ }
282 281 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
283 176 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
284 19 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ℕ )
285 20 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ℝ )
286 116 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
287 186 nnred ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℝ )
288 287 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 𝑦 + 1 ) ∈ ℝ )
289 simpr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ≤ 𝑦 )
290 116 lep1d ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑦 + 1 ) )
291 290 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 ≤ ( 𝑦 + 1 ) )
292 285 286 288 289 291 letrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) )
293 fznn ( ( 𝑦 + 1 ) ∈ ℤ → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
294 187 293 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
295 294 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
296 284 292 295 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) )
297 51 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℕ )
298 1red ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 1 ∈ ℝ )
299 285 286 298 289 leadd1dd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) )
300 fznn ( ( 𝑦 + 1 ) ∈ ℤ → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
301 187 300 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
302 301 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
303 297 299 302 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) )
304 prssi ( ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ∧ ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) )
305 296 303 304 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) )
306 imass2 ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
307 305 306 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
308 283 307 eqsstrrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
309 282 308 eqssd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
310 215 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
311 309 310 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
312 undif ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
313 305 312 sylib ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
314 313 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
315 225 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
316 eluzp1p1 ( ( 𝑁 − 1 ) ∈ ( ℤ𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
317 150 316 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
318 317 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
319 149 318 eqeltrrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
320 fzss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
321 319 320 syl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
322 321 ssdifd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
323 322 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
324 resiima ( ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
325 323 324 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
326 315 325 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ∅ ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
327 imaundi ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
328 uncom ( ∅ ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ )
329 un0 ( ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
330 328 329 eqtr2i ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ∅ ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
331 326 327 330 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
332 314 331 eqtr3d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
333 311 332 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
334 280 333 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
335 334 313 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
336 335 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
337 279 336 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
338 337 xpeq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
339 imaco ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
340 112 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
341 incom ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
342 126 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℝ )
343 186 peano2nnd ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℕ )
344 343 nnred ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ )
345 344 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ )
346 21 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( ( 2nd𝑇 ) + 1 ) )
347 116 ltp1d ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 < ( 𝑦 + 1 ) )
348 347 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 < ( 𝑦 + 1 ) )
349 285 286 288 289 348 lelttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( 𝑦 + 1 ) )
350 285 288 298 349 ltadd1dd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) )
351 285 342 345 346 350 lttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) )
352 ltnle ( ( ( 2nd𝑇 ) ∈ ℝ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
353 20 344 352 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
354 353 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
355 351 354 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) )
356 elfzle1 ( ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) )
357 355 356 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
358 disjsn ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) = ∅ ↔ ¬ ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
359 357 358 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) = ∅ )
360 ltnle ( ( ( ( 2nd𝑇 ) + 1 ) ∈ ℝ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
361 126 344 360 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
362 361 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
363 350 362 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) )
364 elfzle1 ( ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) )
365 363 364 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
366 disjsn ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
367 365 366 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
368 359 367 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ∅ ∪ ∅ ) )
369 140 ineq2i ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) )
370 indi ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) )
371 369 370 eqtr2i ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
372 368 371 144 3eqtr3g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
373 341 372 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
374 fnimadisj ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∧ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
375 340 373 374 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
376 343 227 eleqtrdi ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ ‘ 1 ) )
377 fzss1 ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
378 reldisj ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
379 376 377 378 3syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
380 379 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
381 372 380 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
382 resiima ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
383 381 382 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
384 375 383 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
385 imaundir ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
386 uncom ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∪ ∅ )
387 un0 ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∪ ∅ ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 )
388 386 387 eqtr2i ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
389 384 385 388 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
390 389 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
391 339 390 syl5eq ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
392 391 xpeq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
393 338 392 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
394 278 393 syldan ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
395 394 oveq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
396 iffalse ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
397 396 csbeq1d ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑦 + 1 ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
398 ovex ( 𝑦 + 1 ) ∈ V
399 oveq2 ( 𝑗 = ( 𝑦 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑦 + 1 ) ) )
400 399 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
401 400 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
402 oveq1 ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
403 402 oveq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
404 403 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
405 404 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
406 401 405 uneq12d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
407 406 oveq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
408 398 407 csbie ( 𝑦 + 1 ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
409 397 408 eqtrdi ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
410 409 adantl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
411 396 csbeq1d ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑦 + 1 ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
412 399 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
413 412 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
414 403 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
415 414 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
416 413 415 uneq12d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
417 416 oveq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
418 398 417 csbie ( 𝑦 + 1 ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
419 411 418 eqtrdi ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
420 419 adantl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
421 395 410 420 3eqtr4d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
422 275 421 pm2.61dan ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
423 422 mpteq2dva ( 𝜑 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
424 109 423 eqtr4d ( 𝜑𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
425 opex ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∈ V
426 425 24 op1std ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ )
427 425 24 op2ndd ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → ( 2nd𝑡 ) = ( 2nd𝑇 ) )
428 breq2 ( ( 2nd𝑡 ) = ( 2nd𝑇 ) → ( 𝑦 < ( 2nd𝑡 ) ↔ 𝑦 < ( 2nd𝑇 ) ) )
429 428 ifbid ( ( 2nd𝑡 ) = ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
430 429 csbeq1d ( ( 2nd𝑡 ) = ( 2nd𝑇 ) → 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 } ) ) ) )
431 fvex ( 1st ‘ ( 1st𝑇 ) ) ∈ V
432 431 80 op1std ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ → ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
433 431 80 op2ndd ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ → ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) )
434 id ( ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) → ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
435 imaeq1 ( ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) )
436 435 xpeq1d ( ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) )
437 imaeq1 ( ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
438 437 xpeq1d ( ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
439 436 438 uneq12d ( ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) → ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
440 434 439 oveqan12d ( ( ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) ∧ ( 2nd ‘ ( 1st𝑡 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ) → ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
441 432 433 440 syl2anc ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ → ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
442 441 csbeq2dv ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
443 430 442 sylan9eqr ( ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∧ ( 2nd𝑡 ) = ( 2nd𝑇 ) ) → if ( 𝑦 < ( 2nd𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
444 426 427 443 syl2anc ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → if ( 𝑦 < ( 2nd𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑡 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑡 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
445 444 mpteq2dv ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → ( 𝑦 ∈ ( 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𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
446 445 eqeq2d ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → ( 𝐹 = ( 𝑦 ∈ ( 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𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
447 446 2 elrab2 ( ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ 𝑆 ↔ ( ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ ( ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) × ( 0 ... 𝑁 ) ) ∧ 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ) )
448 90 424 447 sylanbrc ( 𝜑 → ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ 𝑆 )