![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatexch1 | Structured version Visualization version GIF version |
Description: Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
Ref | Expression |
---|---|
hlatexchb.l | ⊢ ≤ = (le‘𝐾) |
hlatexchb.j | ⊢ ∨ = (join‘𝐾) |
hlatexchb.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
hlatexch1 | ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlcvl 35918 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
2 | hlatexchb.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
3 | hlatexchb.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
4 | hlatexchb.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | 2, 3, 4 | cvlatexch1 35895 | . 2 ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃))) |
6 | 1, 5 | syl3an1 1143 | 1 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 ≠ wne 2964 class class class wbr 4927 ‘cfv 6186 (class class class)co 6974 lecple 16422 joincjn 17406 Atomscatm 35822 CvLatclc 35824 HLchlt 35909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-rep 5047 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-ral 3090 df-rex 3091 df-reu 3092 df-rab 3094 df-v 3414 df-sbc 3681 df-csb 3786 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-nul 4178 df-if 4349 df-pw 4422 df-sn 4440 df-pr 4442 df-op 4446 df-uni 4711 df-iun 4792 df-br 4928 df-opab 4990 df-mpt 5007 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6935 df-ov 6977 df-oprab 6978 df-proset 17390 df-poset 17408 df-plt 17420 df-lub 17436 df-glb 17437 df-join 17438 df-meet 17439 df-p0 17501 df-lat 17508 df-covers 35825 df-ats 35826 df-atl 35857 df-cvlat 35881 df-hlat 35910 |
This theorem is referenced by: exatleN 35963 3noncolr2 36008 4noncolr3 36012 3atlem4 36045 3atlem6 36047 4atlem0ae 36153 dalem3 36223 dalem5 36226 dalem-cly 36230 dalem28 36259 cdlema1N 36350 cdlemblem 36352 paddasslem2 36380 pmodlem1 36405 osumcllem6N 36520 pexmidlem3N 36531 trlval4 36747 cdlemd3 36759 cdleme3h 36794 cdleme7aa 36801 cdleme11j 36826 cdleme15b 36834 cdlemg27b 37255 |
Copyright terms: Public domain | W3C validator |