Metamath Proof Explorer

Theorem ballotlemsf1o

Description: The defined S is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
Assertion ballotlemsf1o ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
11 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑖 ) = if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) )
12 1 2 3 4 5 6 7 8 9 ballotlemsdom ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
13 11 12 eqeltrrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
14 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
15 1 2 3 4 5 6 7 8 9 ballotlemsdom ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
16 14 15 eqeltrrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 oveq2 ⊢ ( 𝑖 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ) )
18 id ⊢ ( 𝑖 = 𝑗 → 𝑖 = 𝑗 )
19 breq1 ⊢ ( 𝑖 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) → ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ≤ ( 𝐼 ‘ 𝐶 ) ) )
20 breq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ↔ 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ) )
21 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
22 21 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
23 elfzelz ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
24 23 peano2zd ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℤ )
25 22 24 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℤ )
26 25 zcnd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℂ )
27 26 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℂ )
28 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑗 ∈ ℤ )
29 28 zcnd ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑗 ∈ ℂ )
30 29 ad2antll ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑗 ∈ ℂ )
31 27 30 nncand ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ) = 𝑗 )
32 31 eqcomd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ) )
33 22 23 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
34 33 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
35 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑗 ∈ ℕ )
36 35 ad2antll ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑗 ∈ ℕ )
37 34 36 ltesubnnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ≤ ( 𝐼 ‘ 𝐶 ) )
38 37 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ≤ ( 𝐼 ‘ 𝐶 ) )
39 vex ⊢ 𝑗 ∈ V
40 39 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑗 ∈ V )
41 ovexd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) ∈ V )
42 17 18 19 20 32 38 40 41 ifeqeqx ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑖 = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) → 𝑗 = if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) )
43 oveq2 ⊢ ( 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ) )
44 id ⊢ ( 𝑗 = 𝑖 → 𝑗 = 𝑖 )
45 breq1 ⊢ ( 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) → ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ≤ ( 𝐼 ‘ 𝐶 ) ) )
46 breq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ↔ 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ) )
47 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑖 ∈ ℤ )
48 47 zcnd ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑖 ∈ ℂ )
49 48 ad2antrl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑖 ∈ ℂ )
50 27 49 nncand ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ) = 𝑖 )
51 50 eqcomd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑖 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ) )
52 34 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
53 simplrl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
54 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑖 ∈ ℕ )
55 53 54 syl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝑖 ∈ ℕ )
56 52 55 ltesubnnd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ≤ ( 𝐼 ‘ 𝐶 ) )
57 vex ⊢ 𝑖 ∈ V
58 57 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → 𝑖 ∈ V )
59 ovexd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) ∈ V )
60 43 44 45 46 51 56 58 59 ifeqeqx ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) ∧ 𝑗 = if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) → 𝑖 = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
61 42 60 impbida ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ) → ( 𝑖 = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ↔ 𝑗 = if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
62 10 13 16 61 f1o3d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) ) )
63 62 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
64 oveq2 ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) )
65 20 64 18 ifbieq12d ⊢ ( 𝑖 = 𝑗 → if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
66 65 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
67 66 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) )
68 62 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) )
69 67 10 68 3eqtr4rd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) )
70 63 69 jca ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) ) )