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 | ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑋 ) |