Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lhpat | 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, 23-May-2012.) |
Ref | Expression |
---|---|
lhpat.l | β’ β€ = (leβπΎ) |
lhpat.j | β’ β¨ = (joinβπΎ) |
lhpat.m | β’ β§ = (meetβπΎ) |
lhpat.a | β’ π΄ = (AtomsβπΎ) |
lhpat.h | β’ π» = (LHypβπΎ) |
Ref | Expression |
---|---|
lhpat | β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β ((π β¨ π) β§ π) β π΄) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1l 1198 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β πΎ β HL) | |
2 | simp2l 1200 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | |
3 | simp3l 1202 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | |
4 | simp1r 1199 | . . 3 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π») | |
5 | eqid 2738 | . . . 4 β’ (BaseβπΎ) = (BaseβπΎ) | |
6 | lhpat.h | . . . 4 β’ π» = (LHypβπΎ) | |
7 | 5, 6 | lhpbase 38347 | . . 3 β’ (π β π» β π β (BaseβπΎ)) |
8 | 4, 7 | syl 17 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β (BaseβπΎ)) |
9 | simp3r 1203 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π) | |
10 | eqid 2738 | . . . 4 β’ (1.βπΎ) = (1.βπΎ) | |
11 | eqid 2738 | . . . 4 β’ ( β βπΎ) = ( β βπΎ) | |
12 | 10, 11, 6 | lhp1cvr 38348 | . . 3 β’ ((πΎ β HL β§ π β π») β π( β βπΎ)(1.βπΎ)) |
13 | 12 | 3ad2ant1 1134 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π( β βπΎ)(1.βπΎ)) |
14 | simp2r 1201 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β Β¬ π β€ π) | |
15 | lhpat.l | . . 3 β’ β€ = (leβπΎ) | |
16 | lhpat.j | . . 3 β’ β¨ = (joinβπΎ) | |
17 | lhpat.m | . . 3 β’ β§ = (meetβπΎ) | |
18 | lhpat.a | . . 3 β’ π΄ = (AtomsβπΎ) | |
19 | 5, 15, 16, 17, 10, 11, 18 | 1cvrat 37825 | . 2 β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β (BaseβπΎ)) β§ (π β π β§ π( β βπΎ)(1.βπΎ) β§ Β¬ π β€ π)) β ((π β¨ π) β§ π) β π΄) |
20 | 1, 2, 3, 8, 9, 13, 14, 19 | syl133anc 1394 | 1 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β ((π β¨ π) β§ π) β π΄) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β§ wa 397 β§ w3a 1088 = wceq 1542 β wcel 2107 β wne 2942 class class class wbr 5104 βcfv 6492 (class class class)co 7350 Basecbs 17018 lecple 17075 joincjn 18135 meetcmee 18136 1.cp1 18248 β ccvr 37610 Atomscatm 37611 HLchlt 37698 LHypclh 38333 |
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 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 |
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 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7306 df-ov 7353 df-oprab 7354 df-proset 18119 df-poset 18137 df-plt 18154 df-lub 18170 df-glb 18171 df-join 18172 df-meet 18173 df-p0 18249 df-p1 18250 df-lat 18256 df-clat 18323 df-oposet 37524 df-ol 37526 df-oml 37527 df-covers 37614 df-ats 37615 df-atl 37646 df-cvlat 37670 df-hlat 37699 df-lhyp 38337 |
This theorem is referenced by: lhpat2 38394 4atexlemex6 38423 trlat 38518 cdlemc5 38544 cdleme3e 38581 cdleme7b 38593 cdleme11k 38617 cdleme16e 38631 cdleme16f 38632 cdlemeda 38647 cdleme22cN 38691 cdleme22d 38692 cdleme23b 38699 cdlemf2 38911 cdlemg12g 38998 cdlemg17dALTN 39013 cdlemg19a 39032 |
Copyright terms: Public domain | W3C validator |