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 eqtrid ( ( ( 𝜑𝑦 ∈ ( 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 eqtrid ( ( ( 𝜑𝑦 ∈ ( 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 disjdifr ( ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅
223 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 ) } ) = ∅ )
224 221 222 223 mp2an ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅
225 224 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
226 nnuz ℕ = ( ℤ ‘ 1 )
227 186 226 eleqtrdi ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( ℤ ‘ 1 ) )
228 fzss1 ( ( 𝑦 + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
229 227 228 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
230 229 ssdifd ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
231 resiima ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
232 230 231 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
233 232 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
234 225 233 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 ) } ) ) )
235 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 ) } ) ) )
236 uncom ( ∅ ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ )
237 un0 ( ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
238 236 237 eqtr2i ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
239 234 235 238 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
240 220 239 eqtr3d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
241 217 240 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
242 172 241 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( ( 𝑦 + 1 ) ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
243 242 219 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
244 243 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
245 171 244 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
246 245 xpeq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < ( 2nd𝑇 ) ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
247 170 246 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 } ) ) )
248 247 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 } ) ) ) )
249 iftrue ( 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
250 249 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 } ) ) ) )
251 vex 𝑦 ∈ V
252 oveq2 ( 𝑗 = 𝑦 → ( 1 ... 𝑗 ) = ( 1 ... 𝑦 ) )
253 252 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 ... 𝑦 ) ) )
254 253 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 } ) )
255 oveq1 ( 𝑗 = 𝑦 → ( 𝑗 + 1 ) = ( 𝑦 + 1 ) )
256 255 oveq1d ( 𝑗 = 𝑦 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑦 + 1 ) ... 𝑁 ) )
257 256 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 ) ... 𝑁 ) ) )
258 257 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 } ) )
259 254 258 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 } ) ) )
260 259 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 } ) ) ) )
261 251 260 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 } ) ) )
262 250 261 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 } ) ) ) )
263 262 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 } ) ) ) )
264 249 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 } ) ) ) )
265 252 imaeq2d ( 𝑗 = 𝑦 → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) )
266 265 xpeq1d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) )
267 256 imaeq2d ( 𝑗 = 𝑦 → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) )
268 267 xpeq1d ( 𝑗 = 𝑦 → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) )
269 266 268 uneq12d ( 𝑗 = 𝑦 → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
270 269 oveq2d ( 𝑗 = 𝑦 → ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
271 251 270 csbie 𝑦 / 𝑗 ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ∘f + ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑦 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑦 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
272 264 271 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 } ) ) ) )
273 272 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 } ) ) ) )
274 248 263 273 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 } ) ) ) )
275 lenlt ( ( ( 2nd𝑇 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 2nd𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2nd𝑇 ) ) )
276 20 116 275 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) ≤ 𝑦 ↔ ¬ 𝑦 < ( 2nd𝑇 ) ) )
277 276 biimpar ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < ( 2nd𝑇 ) ) → ( 2nd𝑇 ) ≤ 𝑦 )
278 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 ) ) ) )
279 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 ) ) ) )
280 imassrn ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ }
281 280 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) ⊆ ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
282 176 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
283 19 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ℕ )
284 20 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ℝ )
285 116 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
286 186 nnred ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ℝ )
287 286 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 𝑦 + 1 ) ∈ ℝ )
288 simpr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ≤ 𝑦 )
289 116 lep1d ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑦 + 1 ) )
290 289 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 ≤ ( 𝑦 + 1 ) )
291 284 285 287 288 290 letrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) )
292 fznn ( ( 𝑦 + 1 ) ∈ ℤ → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
293 187 292 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
294 293 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( 2nd𝑇 ) ∈ ℕ ∧ ( 2nd𝑇 ) ≤ ( 𝑦 + 1 ) ) ) )
295 283 291 294 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) )
296 51 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℕ )
297 1red ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 1 ∈ ℝ )
298 284 285 297 288 leadd1dd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) )
299 fznn ( ( 𝑦 + 1 ) ∈ ℤ → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
300 187 299 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
301 300 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( ( ( 2nd𝑇 ) + 1 ) ∈ ℕ ∧ ( ( 2nd𝑇 ) + 1 ) ≤ ( 𝑦 + 1 ) ) ) )
302 296 298 301 mpbir2and ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) )
303 prssi ( ( ( 2nd𝑇 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ∧ ( ( 2nd𝑇 ) + 1 ) ∈ ( 1 ... ( 𝑦 + 1 ) ) ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) )
304 295 302 303 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) )
305 imass2 ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
306 304 305 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
307 282 306 eqsstrrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ⊆ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) )
308 281 307 eqssd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) = ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } )
309 215 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ran { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
310 308 309 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( 1 ... ( 𝑦 + 1 ) ) ) = { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
311 undif ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ⊆ ( 1 ... ( 𝑦 + 1 ) ) ↔ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
312 304 311 sylib ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
313 312 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
314 224 a1i ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
315 eluzp1p1 ( ( 𝑁 − 1 ) ∈ ( ℤ𝑦 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
316 150 315 syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
317 316 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
318 149 317 eqeltrrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) )
319 fzss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑦 + 1 ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
320 318 319 syl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 ... ( 𝑦 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
321 320 ssdifd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
322 321 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
323 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 ) } ) )
324 322 323 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
325 314 324 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 ) } ) ) )
326 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 ) } ) ) )
327 uncom ( ∅ ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ )
328 un0 ( ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ∪ ∅ ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
329 327 328 eqtr2i ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ∅ ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
330 325 326 329 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
331 313 330 eqtr3d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
332 310 331 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 ) } ) ) )
333 279 332 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∪ ( ( 1 ... ( 𝑦 + 1 ) ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
334 333 312 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( 1 ... ( 𝑦 + 1 ) ) )
335 334 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
336 278 335 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
337 336 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 } ) )
338 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 ) ... 𝑁 ) ) )
339 112 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
340 incom ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
341 126 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) ∈ ℝ )
342 186 peano2nnd ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℕ )
343 342 nnred ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ )
344 343 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ )
345 21 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( ( 2nd𝑇 ) + 1 ) )
346 116 ltp1d ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 < ( 𝑦 + 1 ) )
347 346 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → 𝑦 < ( 𝑦 + 1 ) )
348 284 285 287 288 347 lelttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( 𝑦 + 1 ) )
349 284 287 297 348 ltadd1dd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) )
350 284 341 344 345 349 lttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) )
351 ltnle ( ( ( 2nd𝑇 ) ∈ ℝ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
352 20 343 351 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
353 352 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd𝑇 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) ) )
354 350 353 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) )
355 elfzle1 ( ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝑦 + 1 ) + 1 ) ≤ ( 2nd𝑇 ) )
356 354 355 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
357 disjsn ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) = ∅ ↔ ¬ ( 2nd𝑇 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
358 356 357 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) = ∅ )
359 ltnle ( ( ( ( 2nd𝑇 ) + 1 ) ∈ ℝ ∧ ( ( 𝑦 + 1 ) + 1 ) ∈ ℝ ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
360 126 343 359 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
361 360 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd𝑇 ) + 1 ) < ( ( 𝑦 + 1 ) + 1 ) ↔ ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) ) )
362 349 361 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) )
363 elfzle1 ( ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝑦 + 1 ) + 1 ) ≤ ( ( 2nd𝑇 ) + 1 ) )
364 362 363 nsyl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
365 disjsn ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ¬ ( ( 2nd𝑇 ) + 1 ) ∈ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
366 364 365 sylibr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
367 358 366 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ∅ ∪ ∅ ) )
368 140 ineq2i ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) )
369 indi ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ ( { ( 2nd𝑇 ) } ∪ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) )
370 368 369 eqtr2i ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) } ) ∪ ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( ( 2nd𝑇 ) + 1 ) } ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } )
371 367 370 144 3eqtr3g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ )
372 340 371 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
373 fnimadisj ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } Fn { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∧ ( { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ∩ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
374 339 372 373 syl2anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
375 342 226 eleqtrdi ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ ‘ 1 ) )
376 fzss1 ( ( ( 𝑦 + 1 ) + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
377 reldisj ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
378 375 376 377 3syl ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
379 378 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∩ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) = ∅ ↔ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) )
380 371 379 mpbid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) )
381 resiima ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
382 380 381 syl ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
383 374 382 uneq12d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ∪ ( ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
384 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 ) ... 𝑁 ) ) )
385 uncom ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∪ ∅ )
386 un0 ( ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ∪ ∅ ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 )
387 385 386 eqtr2i ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) = ( ∅ ∪ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
388 383 384 387 3eqtr4g ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
389 388 imaeq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
390 338 389 eqtrid ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ( 2nd𝑇 ) ≤ 𝑦 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
391 390 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 } ) )
392 337 391 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 } ) ) )
393 277 392 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 } ) ) )
394 393 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 } ) ) ) )
395 iffalse ( ¬ 𝑦 < ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
396 395 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 } ) ) ) )
397 ovex ( 𝑦 + 1 ) ∈ V
398 oveq2 ( 𝑗 = ( 𝑦 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑦 + 1 ) ) )
399 398 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 ) ) ) )
400 399 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 } ) )
401 oveq1 ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
402 401 oveq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) )
403 402 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 ) ... 𝑁 ) ) )
404 403 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 } ) )
405 400 404 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 } ) ) )
406 405 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 } ) ) ) )
407 397 406 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 } ) ) )
408 396 407 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 } ) ) ) )
409 408 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 } ) ) ) )
410 395 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 } ) ) ) )
411 398 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) )
412 411 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) )
413 402 imaeq2d ( 𝑗 = ( 𝑦 + 1 ) → ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) )
414 413 xpeq1d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
415 412 414 uneq12d ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( 1 ... ( 𝑦 + 1 ) ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 1st𝑇 ) ) “ ( ( ( 𝑦 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
416 415 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 } ) ) ) )
417 397 416 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 } ) ) )
418 410 417 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 } ) ) ) )
419 418 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 } ) ) ) )
420 394 409 419 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 } ) ) ) )
421 274 420 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 } ) ) ) )
422 421 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 } ) ) ) ) )
423 109 422 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 } ) ) ) ) )
424 opex ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ ∈ V
425 424 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 ) } ) ) ) ) ⟩ )
426 424 24 op2ndd ( 𝑡 = ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ → ( 2nd𝑡 ) = ( 2nd𝑇 ) )
427 breq2 ( ( 2nd𝑡 ) = ( 2nd𝑇 ) → ( 𝑦 < ( 2nd𝑡 ) ↔ 𝑦 < ( 2nd𝑇 ) ) )
428 427 ifbid ( ( 2nd𝑡 ) = ( 2nd𝑇 ) → if ( 𝑦 < ( 2nd𝑡 ) , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < ( 2nd𝑇 ) , 𝑦 , ( 𝑦 + 1 ) ) )
429 428 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 } ) ) ) )
430 fvex ( 1st ‘ ( 1st𝑇 ) ) ∈ V
431 430 80 op1std ( ( 1st𝑡 ) = ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ → ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
432 430 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 ) } ) ) ) ) )
433 id ( ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) → ( 1st ‘ ( 1st𝑡 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
434 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 ... 𝑗 ) ) )
435 434 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 } ) )
436 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 ) ... 𝑁 ) ) )
437 436 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 } ) )
438 435 437 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 } ) ) )
439 433 438 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 } ) ) ) )
440 431 432 439 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 } ) ) ) )
441 440 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 } ) ) ) )
442 429 441 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 } ) ) ) )
443 425 426 442 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 } ) ) ) )
444 443 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 } ) ) ) ) )
445 444 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 } ) ) ) ) ) )
446 445 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 } ) ) ) ) ) )
447 90 423 446 sylanbrc ( 𝜑 → ⟨ ⟨ ( 1st ‘ ( 1st𝑇 ) ) , ( ( 2nd ‘ ( 1st𝑇 ) ) ∘ ( { ⟨ ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) ⟩ , ⟨ ( ( 2nd𝑇 ) + 1 ) , ( 2nd𝑇 ) ⟩ } ∪ ( I ↾ ( ( 1 ... 𝑁 ) ∖ { ( 2nd𝑇 ) , ( ( 2nd𝑇 ) + 1 ) } ) ) ) ) ⟩ , ( 2nd𝑇 ) ⟩ ∈ 𝑆 )