Description: Value of [_ R / s ]_ N when -. R .<_ ( P .\/ Q ) . (Contributed by NM, 30-Mar-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdlemefr27.b | |- B = ( Base ` K ) |
|
| cdlemefr27.l | |- .<_ = ( le ` K ) |
||
| cdlemefr27.j | |- .\/ = ( join ` K ) |
||
| cdlemefr27.m | |- ./\ = ( meet ` K ) |
||
| cdlemefr27.a | |- A = ( Atoms ` K ) |
||
| cdlemefr27.h | |- H = ( LHyp ` K ) |
||
| cdlemefr27.u | |- U = ( ( P .\/ Q ) ./\ W ) |
||
| cdlemefr27.c | |- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) |
||
| cdlemefr27.n | |- N = if ( s .<_ ( P .\/ Q ) , I , C ) |
||
| cdleme43fr.x | |- X = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) |
||
| Assertion | cdleme43frv1snN | |- ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdlemefr27.b | |- B = ( Base ` K ) |
|
| 2 | cdlemefr27.l | |- .<_ = ( le ` K ) |
|
| 3 | cdlemefr27.j | |- .\/ = ( join ` K ) |
|
| 4 | cdlemefr27.m | |- ./\ = ( meet ` K ) |
|
| 5 | cdlemefr27.a | |- A = ( Atoms ` K ) |
|
| 6 | cdlemefr27.h | |- H = ( LHyp ` K ) |
|
| 7 | cdlemefr27.u | |- U = ( ( P .\/ Q ) ./\ W ) |
|
| 8 | cdlemefr27.c | |- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) |
|
| 9 | cdlemefr27.n | |- N = if ( s .<_ ( P .\/ Q ) , I , C ) |
|
| 10 | cdleme43fr.x | |- X = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) |
|
| 11 | 8 9 10 | cdleme31sn2 | |- ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = X ) |