Metamath Proof Explorer

Theorem oprpiece1res1

Description: Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010) (Proof shortened by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses oprpiece1.1 ⊢ 𝐴 ∈ ℝ
oprpiece1.2 ⊢ 𝐵 ∈ ℝ
oprpiece1.3 ⊢ 𝐴 ≤ 𝐵
oprpiece1.4 ⊢ 𝑅 ∈ V
oprpiece1.5 ⊢ 𝑆 ∈ V
oprpiece1.6 ⊢ 𝐾 ∈ ( 𝐴 [,] 𝐵 )
oprpiece1.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
oprpiece1.8 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ 𝑅 )
Assertion oprpiece1res1 ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = 𝐺

Proof

Step Hyp Ref Expression
1 oprpiece1.1 ⊢ 𝐴 ∈ ℝ
2 oprpiece1.2 ⊢ 𝐵 ∈ ℝ
3 oprpiece1.3 ⊢ 𝐴 ≤ 𝐵
4 oprpiece1.4 ⊢ 𝑅 ∈ V
5 oprpiece1.5 ⊢ 𝑆 ∈ V
6 oprpiece1.6 ⊢ 𝐾 ∈ ( 𝐴 [,] 𝐵 )
7 oprpiece1.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
8 oprpiece1.8 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ 𝑅 )
9 1 rexri ⊢ 𝐴 ∈ ℝ*
10 2 rexri ⊢ 𝐵 ∈ ℝ*
11 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
12 9 10 3 11 mp3an ⊢ 𝐴 ∈ ( 𝐴 [,] 𝐵 )
13 iccss2 ⊢ ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐾 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 ) )
14 12 6 13 mp2an ⊢ ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 )
15 ssid ⊢ 𝐶 ⊆ 𝐶
16 resmpo ⊢ ( ( ( 𝐴 [,] 𝐾 ) ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ⊆ 𝐶 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) )
17 14 15 16 mp2an ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
18 7 reseq1i ⊢ ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) )
19 eliccxr ⊢ ( 𝐾 ∈ ( 𝐴 [,] 𝐵 ) → 𝐾 ∈ ℝ* )
20 6 19 ax-mp ⊢ 𝐾 ∈ ℝ*
21 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐾 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐾 ) ) → 𝑥 ≤ 𝐾 )
22 9 20 21 mp3an12 ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) → 𝑥 ≤ 𝐾 )
23 22 iftrued ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) → if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) = 𝑅 )
24 23 adantr ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) ∧ 𝑦 ∈ 𝐶 ) → if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) = 𝑅 )
25 24 mpoeq3ia ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ 𝑅 )
26 8 25 eqtr4i ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐾 ) , 𝑦 ∈ 𝐶 ↦ if ( 𝑥 ≤ 𝐾 , 𝑅 , 𝑆 ) )
27 17 18 26 3eqtr4i ⊢ ( 𝐹 ↾ ( ( 𝐴 [,] 𝐾 ) × 𝐶 ) ) = 𝐺