![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lhpat2 | Structured version Visualization version GIF version |
Description: Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.) |
Ref | Expression |
---|---|
lhpat.l | ⊢ ≤ = (le‘𝐾) |
lhpat.j | ⊢ ∨ = (join‘𝐾) |
lhpat.m | ⊢ ∧ = (meet‘𝐾) |
lhpat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
lhpat.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lhpat2.r | ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
Ref | Expression |
---|---|
lhpat2 | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑅 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpat2.r | . 2 ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊) | |
2 | lhpat.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
3 | lhpat.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
4 | lhpat.m | . . 3 ⊢ ∧ = (meet‘𝐾) | |
5 | lhpat.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
6 | lhpat.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
7 | 2, 3, 4, 5, 6 | lhpat 36710 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴) |
8 | 1, 7 | syl5eqel 2887 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑅 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 class class class wbr 4962 ‘cfv 6225 (class class class)co 7016 lecple 16401 joincjn 17383 meetcmee 17384 Atomscatm 35930 HLchlt 36017 LHypclh 36651 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-proset 17367 df-poset 17385 df-plt 17397 df-lub 17413 df-glb 17414 df-join 17415 df-meet 17416 df-p0 17478 df-p1 17479 df-lat 17485 df-clat 17547 df-oposet 35843 df-ol 35845 df-oml 35846 df-covers 35933 df-ats 35934 df-atl 35965 df-cvlat 35989 df-hlat 36018 df-lhyp 36655 |
This theorem is referenced by: lhpat3 36713 4atexlemu 36731 4atexlemv 36732 cdleme0a 36878 cdleme0dN 36883 cdleme0e 36884 cdleme02N 36889 cdleme0ex1N 36890 cdleme0moN 36892 cdleme3b 36896 cdleme3c 36897 cdleme3g 36901 cdleme3h 36902 cdleme3 36904 cdleme7aa 36909 cdleme7c 36912 cdleme7d 36913 cdleme7e 36914 cdleme7ga 36915 cdleme7 36916 cdleme9a 36918 cdleme16aN 36926 cdleme11a 36927 cdleme11c 36928 cdleme12 36938 cdleme16b 36946 cdleme16c 36947 cdleme16d 36948 cdleme20h 36983 cdleme20j 36985 cdleme20l2 36988 cdlemeg46rgv 37195 cdlemeg46req 37196 |
Copyright terms: Public domain | W3C validator |