![]() |
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 1915 | . . . . 5 ⊢ Ⅎ𝑠 𝑅 ≤ (𝑃 ∨ 𝑄) | |
2 | nfcsb1v 3852 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐼 | |
3 | nfcsb1v 3852 | . . . . 5 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐷 | |
4 | 1, 2, 3 | nfif 4454 | . . . 4 ⊢ Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) |
5 | 4 | a1i 11 | . . 3 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
6 | breq1 5033 | . . . 4 ⊢ (𝑠 = 𝑅 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑅 ≤ (𝑃 ∨ 𝑄))) | |
7 | csbeq1a 3842 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐼 = ⦋𝑅 / 𝑠⦌𝐼) | |
8 | csbeq1a 3842 | . . . 4 ⊢ (𝑠 = 𝑅 → 𝐷 = ⦋𝑅 / 𝑠⦌𝐷) | |
9 | 6, 7, 8 | ifbieq12d 4452 | . . 3 ⊢ (𝑠 = 𝑅 → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
10 | 5, 9 | csbiegf 3861 | . 2 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)) |
11 | cdleme31sn.n | . . 3 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) | |
12 | 11 | csbeq2i 3836 | . 2 ⊢ ⦋𝑅 / 𝑠⦌𝑁 = ⦋𝑅 / 𝑠⦌if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
13 | cdleme31sn.c | . 2 ⊢ 𝐶 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) | |
14 | 10, 12, 13 | 3eqtr4g 2858 | 1 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 Ⅎwnfc 2936 ⦋csb 3828 ifcif 4425 class class class wbr 5030 (class class class)co 7135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-un 3886 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 |
This theorem is referenced by: cdleme31sn1 37677 cdleme31sn2 37685 |
Copyright terms: Public domain | W3C validator |