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 | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| cdlemefr27.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
| cdlemefr27.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| cdlemefr27.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| cdlemefr27.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| cdlemefr27.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| cdlemefr27.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | ||
| cdlemefr27.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | ||
| cdlemefr27.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | ||
| cdleme43fr.x | ⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) | ||
| Assertion | cdleme43frv1snN | ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdlemefr27.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| 2 | cdlemefr27.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 3 | cdlemefr27.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 4 | cdlemefr27.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 5 | cdlemefr27.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 6 | cdlemefr27.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 7 | cdlemefr27.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | |
| 8 | cdlemefr27.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | |
| 9 | cdlemefr27.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | |
| 10 | cdleme43fr.x | ⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) | |
| 11 | 8 9 10 | cdleme31sn2 | ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑋 ) |