Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cvrat42 | Structured version Visualization version GIF version |
Description: Commuted version of cvrat4 37760. (Contributed by NM, 28-Jan-2012.) |
Ref | Expression |
---|---|
cvrat4.b | ⊢ 𝐵 = (Base‘𝐾) |
cvrat4.l | ⊢ ≤ = (le‘𝐾) |
cvrat4.j | ⊢ ∨ = (join‘𝐾) |
cvrat4.z | ⊢ 0 = (0.‘𝐾) |
cvrat4.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
cvrat42 | ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑟 ∨ 𝑄)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvrat4.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
2 | cvrat4.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
3 | cvrat4.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
4 | cvrat4.z | . . 3 ⊢ 0 = (0.‘𝐾) | |
5 | cvrat4.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
6 | 1, 2, 3, 4, 5 | cvrat4 37760 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))) |
7 | hllat 37679 | . . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
8 | 7 | ad2antrr 724 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat) |
9 | simplr3 1217 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴) | |
10 | 1, 5 | atbase 37605 | . . . . . . 7 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
11 | 9, 10 | syl 17 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵) |
12 | 1, 5 | atbase 37605 | . . . . . . 7 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵) |
13 | 12 | adantl 483 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵) |
14 | 1, 3 | latjcom 18263 | . . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑄 ∨ 𝑟) = (𝑟 ∨ 𝑄)) |
15 | 8, 11, 13, 14 | syl3anc 1371 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑄 ∨ 𝑟) = (𝑟 ∨ 𝑄)) |
16 | 15 | breq2d 5109 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑃 ≤ (𝑟 ∨ 𝑄))) |
17 | 16 | anbi2d 630 | . . 3 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → ((𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑟 ∨ 𝑄)))) |
18 | 17 | rexbidva 3170 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑟 ∨ 𝑄)))) |
19 | 6, 18 | sylibd 238 | 1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑟 ∨ 𝑄)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∃wrex 3071 class class class wbr 5097 ‘cfv 6484 (class class class)co 7342 Basecbs 17010 lecple 17067 joincjn 18127 0.cp0 18239 Latclat 18247 Atomscatm 37579 HLchlt 37666 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5234 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4858 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5181 df-id 5523 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-riota 7298 df-ov 7345 df-oprab 7346 df-proset 18111 df-poset 18129 df-plt 18146 df-lub 18162 df-glb 18163 df-join 18164 df-meet 18165 df-p0 18241 df-lat 18248 df-clat 18315 df-oposet 37492 df-ol 37494 df-oml 37495 df-covers 37582 df-ats 37583 df-atl 37614 df-cvlat 37638 df-hlat 37667 |
This theorem is referenced by: pmapjat1 38170 djhcvat42 39732 |
Copyright terms: Public domain | W3C validator |