Theorem oprpiece1res1 25219

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.)

Hypotheses

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

Assertion

Ref	Expression
oprpiece1res1	⊢ (𝐹 ↾ ((𝐴[,]𝐾) × 𝐶)) = 𝐺

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐾,𝑦

Allowed substitution hints:   𝑅(𝑥, 𝑦)   𝑆(𝑥, 𝑦)   𝐹(𝑥, 𝑦)   𝐺(𝑥, 𝑦)

Proof of Theorem oprpiece1res1

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899  ifcif 4482   class class class wbr 5103   × cxp 5646   ↾ cres 5650  (class class class)co 7409   ∈ cmpo 7411  ℝcr 11156  ℝ^*cxr 11299   ≤ cle 11301  [,]cicc 13434

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214  ax-pre-lttri 11231  ax-pre-lttrn 11232

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7985  df-2nd 7986  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306  df-icc 13438

This theorem is used by: (None)