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 ⊢ A ∈ ℝ
oprpiece1.2 ⊢ B ∈ ℝ
oprpiece1.3 ⊢ A ≤ B
oprpiece1.4 ⊢ R ∈ V
oprpiece1.5 ⊢ S ∈ V
oprpiece1.6 ⊢ K ∈ A B
oprpiece1.7 ⊢ F = x ∈ A B , y ∈ C ⟼ if x ≤ K R S
oprpiece1.8 ⊢ G = x ∈ A K , y ∈ C ⟼ R
Assertion oprpiece1res1 ⊢ F ↾ A K × C = G

Proof

Step Hyp Ref Expression
1 oprpiece1.1 ⊢ A ∈ ℝ
2 oprpiece1.2 ⊢ B ∈ ℝ
3 oprpiece1.3 ⊢ A ≤ B
4 oprpiece1.4 ⊢ R ∈ V
5 oprpiece1.5 ⊢ S ∈ V
6 oprpiece1.6 ⊢ K ∈ A B
7 oprpiece1.7 ⊢ F = x ∈ A B , y ∈ C ⟼ if x ≤ K R S
8 oprpiece1.8 ⊢ G = x ∈ A K , y ∈ C ⟼ R
9 1 rexri ⊢ A ∈ ℝ *
10 2 rexri ⊢ B ∈ ℝ *
11 lbicc2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A ∈ A B
12 9 10 3 11 mp3an ⊢ A ∈ A B
13 iccss2 ⊢ A ∈ A B ∧ K ∈ A B → A K ⊆ A B
14 12 6 13 mp2an ⊢ A K ⊆ A B
15 ssid ⊢ C ⊆ C
16 resmpo ⊢ A K ⊆ A B ∧ C ⊆ C → x ∈ A B , y ∈ C ⟼ if x ≤ K R S ↾ A K × C = x ∈ A K , y ∈ C ⟼ if x ≤ K R S
17 14 15 16 mp2an ⊢ x ∈ A B , y ∈ C ⟼ if x ≤ K R S ↾ A K × C = x ∈ A K , y ∈ C ⟼ if x ≤ K R S
18 7 reseq1i ⊢ F ↾ A K × C = x ∈ A B , y ∈ C ⟼ if x ≤ K R S ↾ A K × C
19 eliccxr ⊢ K ∈ A B → K ∈ ℝ *
20 6 19 ax-mp ⊢ K ∈ ℝ *
21 iccleub ⊢ A ∈ ℝ * ∧ K ∈ ℝ * ∧ x ∈ A K → x ≤ K
22 9 20 21 mp3an12 ⊢ x ∈ A K → x ≤ K
23 22 iftrued ⊢ x ∈ A K → if x ≤ K R S = R
24 23 adantr ⊢ x ∈ A K ∧ y ∈ C → if x ≤ K R S = R
25 24 mpoeq3ia ⊢ x ∈ A K , y ∈ C ⟼ if x ≤ K R S = x ∈ A K , y ∈ C ⟼ R
26 8 25 eqtr4i ⊢ G = x ∈ A K , y ∈ C ⟼ if x ≤ K R S
27 17 18 26 3eqtr4i ⊢ F ↾ A K × C = G