Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme31sn | Structured version Visualization version GIF version |
Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Ref | Expression |
---|---|
cdleme31sn.n | ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
cdleme31sn.c | ⊢ 𝐶 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) |
Ref | Expression |
---|---|
cdleme31sn | ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1906 | . . . . 5 ⊢ Ⅎ𝑠 𝑅 ≤ (𝑃 ∨ 𝑄) | |
2 | nfcsb1v 3904 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐼 | |
3 | nfcsb1v 3904 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐷 | |
4 | 1, 2, 3 | nfif 4492 | . . . 4 ⊢ Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) |
5 | 4 | a1i 11 | . . 3 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
6 | breq1 5060 | . . . 4 ⊢ (𝑠 = 𝑅 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑅 ≤ (𝑃 ∨ 𝑄))) | |
7 | csbeq1a 3894 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐼 = ⦋𝑅 / 𝑠⦌𝐼) | |
8 | csbeq1a 3894 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐷 = ⦋𝑅 / 𝑠⦌𝐷) | |
9 | 6, 7, 8 | ifbieq12d 4490 | . . 3 ⊢ (𝑠 = 𝑅 → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
10 | 5, 9 | csbiegf 3913 | . 2 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
11 | cdleme31sn.n | . . 3 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) | |
12 | 11 | csbeq2i 3888 | . 2 ⊢ ⦋𝑅 / 𝑠⦌𝑁 = ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
13 | cdleme31sn.c | . 2 ⊢ 𝐶 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) | |
14 | 10, 12, 13 | 3eqtr4g 2878 | 1 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 Ⅎwnfc 2958 ⦋csb 3880 ifcif 4463 class class class wbr 5057 (class class class)co 7145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 |
This theorem is referenced by: cdleme31sn1 37397 cdleme31sn2 37405 |
Copyright terms: Public domain | W3C validator |