Description: Show that [_ R / s ]_ N is an atom not under W when -. R .<_ ( P .\/ Q ) . (Contributed by NM, 6-Mar-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdleme32.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| cdleme32.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
| cdleme32.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| cdleme32.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| cdleme32.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| cdleme32.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| cdleme32.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | ||
| cdleme32.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | ||
| cdleme32.d | ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | ||
| cdleme32.e | ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | ||
| cdleme32.i | ⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) | ||
| cdleme32.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | ||
| Assertion | cdleme32sn2awN | ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ∈ 𝐴 ∧ ¬ ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ≤ 𝑊 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdleme32.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| 2 | cdleme32.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 3 | cdleme32.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 4 | cdleme32.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 5 | cdleme32.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 6 | cdleme32.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 7 | cdleme32.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | |
| 8 | cdleme32.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | |
| 9 | cdleme32.d | ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | |
| 10 | cdleme32.e | ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | |
| 11 | cdleme32.i | ⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) | |
| 12 | cdleme32.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | |
| 13 | 1 2 3 4 5 6 7 8 12 | cdlemefr32sn2aw | ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ∈ 𝐴 ∧ ¬ ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ≤ 𝑊 ) ) |