![]() |
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 1916 | . . . . 5 ⊢ Ⅎ𝑠 𝑅 ≤ (𝑃 ∨ 𝑄) | |
2 | nfcsb1v 3918 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐼 | |
3 | nfcsb1v 3918 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐷 | |
4 | 1, 2, 3 | nfif 4558 | . . . 4 ⊢ Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) |
5 | 4 | a1i 11 | . . 3 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
6 | breq1 5151 | . . . 4 ⊢ (𝑠 = 𝑅 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑅 ≤ (𝑃 ∨ 𝑄))) | |
7 | csbeq1a 3907 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐼 = ⦋𝑅 / 𝑠⦌𝐼) | |
8 | csbeq1a 3907 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐷 = ⦋𝑅 / 𝑠⦌𝐷) | |
9 | 6, 7, 8 | ifbieq12d 4556 | . . 3 ⊢ (𝑠 = 𝑅 → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
10 | 5, 9 | csbiegf 3927 | . 2 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
11 | cdleme31sn.n | . . 3 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) | |
12 | 11 | csbeq2i 3901 | . 2 ⊢ ⦋𝑅 / 𝑠⦌𝑁 = ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
13 | cdleme31sn.c | . 2 ⊢ 𝐶 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) | |
14 | 10, 12, 13 | 3eqtr4g 2796 | 1 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 Ⅎwnfc 2882 ⦋csb 3893 ifcif 4528 class class class wbr 5148 (class class class)co 7412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 |
This theorem is referenced by: cdleme31sn1 39556 cdleme31sn2 39564 |
Copyright terms: Public domain | W3C validator |