![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lhpocnel2 | Structured version Visualization version GIF version |
Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014.) |
Ref | Expression |
---|---|
lhpocnel2.l | ⊢ ≤ = (le‘𝐾) |
lhpocnel2.a | ⊢ 𝐴 = (Atoms‘𝐾) |
lhpocnel2.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lhpocnel2.p | ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
lhpocnel2 | ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpocnel2.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
2 | eqid 2733 | . . 3 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
3 | lhpocnel2.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | lhpocnel2.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
5 | 1, 2, 3, 4 | lhpocnel 38795 | . 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊) ≤ 𝑊)) |
6 | lhpocnel2.p | . . . 4 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) | |
7 | 6 | eleq1i 2825 | . . 3 ⊢ (𝑃 ∈ 𝐴 ↔ ((oc‘𝐾)‘𝑊) ∈ 𝐴) |
8 | 6 | breq1i 5151 | . . . 4 ⊢ (𝑃 ≤ 𝑊 ↔ ((oc‘𝐾)‘𝑊) ≤ 𝑊) |
9 | 8 | notbii 320 | . . 3 ⊢ (¬ 𝑃 ≤ 𝑊 ↔ ¬ ((oc‘𝐾)‘𝑊) ≤ 𝑊) |
10 | 7, 9 | anbi12i 628 | . 2 ⊢ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ↔ (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊) ≤ 𝑊)) |
11 | 5, 10 | sylibr 233 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 class class class wbr 5144 ‘cfv 6535 lecple 17191 occoc 17192 Atomscatm 38039 HLchlt 38126 LHypclh 38761 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5359 ax-pr 5423 ax-un 7712 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-iun 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6487 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7352 df-ov 7399 df-oprab 7400 df-proset 18235 df-poset 18253 df-plt 18270 df-lub 18286 df-glb 18287 df-meet 18289 df-p0 18365 df-p1 18366 df-lat 18372 df-oposet 37952 df-ol 37954 df-oml 37955 df-covers 38042 df-ats 38043 df-atl 38074 df-cvlat 38098 df-hlat 38127 df-lhyp 38765 |
This theorem is referenced by: cdlemk56w 39750 diclspsn 39971 cdlemn3 39974 cdlemn4 39975 cdlemn4a 39976 cdlemn6 39979 cdlemn8 39981 cdlemn9 39982 cdlemn11a 39984 dihordlem7b 39992 dihopelvalcpre 40025 dihmeetlem1N 40067 dihglblem5apreN 40068 dihglbcpreN 40077 dihmeetlem4preN 40083 dihmeetlem13N 40096 dih1dimatlem0 40105 dih1dimatlem 40106 dihpN 40113 dihatexv 40115 dihjatcclem3 40197 dihjatcclem4 40198 |
Copyright terms: Public domain | W3C validator |