Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme3fa | Structured version Visualization version GIF version |
Description: Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 38230. (Contributed by NM, 6-Oct-2012.) |
Ref | Expression |
---|---|
cdleme1.l | ⊢ ≤ = (le‘𝐾) |
cdleme1.j | ⊢ ∨ = (join‘𝐾) |
cdleme1.m | ⊢ ∧ = (meet‘𝐾) |
cdleme1.a | ⊢ 𝐴 = (Atoms‘𝐾) |
cdleme1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
cdleme1.u | ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
cdleme1.f | ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) |
Ref | Expression |
---|---|
cdleme3fa | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐹 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme1.l | . 2 ⊢ ≤ = (le‘𝐾) | |
2 | cdleme1.j | . 2 ⊢ ∨ = (join‘𝐾) | |
3 | cdleme1.m | . 2 ⊢ ∧ = (meet‘𝐾) | |
4 | cdleme1.a | . 2 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | cdleme1.h | . 2 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | cdleme1.u | . 2 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) | |
7 | cdleme1.f | . 2 ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) | |
8 | eqid 2739 | . 2 ⊢ ((𝑃 ∨ 𝑅) ∧ 𝑊) = ((𝑃 ∨ 𝑅) ∧ 𝑊) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cdleme3h 38228 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐹 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1541 ∈ wcel 2109 ≠ wne 2944 class class class wbr 5078 ‘cfv 6430 (class class class)co 7268 lecple 16950 joincjn 18010 meetcmee 18011 Atomscatm 37256 HLchlt 37343 LHypclh 37977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-reu 3072 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-iun 4931 df-iin 4932 df-br 5079 df-opab 5141 df-mpt 5162 df-id 5488 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-1st 7817 df-2nd 7818 df-proset 17994 df-poset 18012 df-plt 18029 df-lub 18045 df-glb 18046 df-join 18047 df-meet 18048 df-p0 18124 df-p1 18125 df-lat 18131 df-clat 18198 df-oposet 37169 df-ol 37171 df-oml 37172 df-covers 37259 df-ats 37260 df-atl 37291 df-cvlat 37315 df-hlat 37344 df-lines 37494 df-psubsp 37496 df-pmap 37497 df-padd 37789 df-lhyp 37981 |
This theorem is referenced by: cdleme3 38230 cdleme7d 38239 cdleme7ga 38241 cdleme11j 38260 cdleme11k 38261 cdleme11 38263 cdleme14 38266 cdleme15a 38267 cdleme16b 38272 cdleme16c 38273 cdleme16d 38274 cdleme16e 38275 cdleme16f 38276 cdleme19d 38299 cdleme20f 38307 cdleme20l1 38313 cdleme20l2 38314 cdleme22f2 38340 cdleme22g 38341 cdlemefr32sn2aw 38397 cdleme35a 38441 cdleme36m 38454 cdleme43bN 38483 |
Copyright terms: Public domain | W3C validator |