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 1197 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β πΎ β HL) | |
2 | simp2l 1199 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | |
3 | simp3l 1201 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | |
4 | simp1r 1198 | . . 3 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π») | |
5 | eqid 2737 | . . . 4 β’ (BaseβπΎ) = (BaseβπΎ) | |
6 | lhpat.h | . . . 4 β’ π» = (LHypβπΎ) | |
7 | 5, 6 | lhpbase 38356 | . . 3 β’ (π β π» β π β (BaseβπΎ)) |
8 | 4, 7 | syl 17 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β (BaseβπΎ)) |
9 | simp3r 1202 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π) | |
10 | eqid 2737 | . . . 4 β’ (1.βπΎ) = (1.βπΎ) | |
11 | eqid 2737 | . . . 4 β’ ( β βπΎ) = ( β βπΎ) | |
12 | 10, 11, 6 | lhp1cvr 38357 | . . 3 β’ ((πΎ β HL β§ π β π») β π( β βπΎ)(1.βπΎ)) |
13 | 12 | 3ad2ant1 1133 | . 2 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π( β βπΎ)(1.βπΎ)) |
14 | simp2r 1200 | . 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 37834 | . 2 β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β (BaseβπΎ)) β§ (π β π β§ π( β βπΎ)(1.βπΎ) β§ Β¬ π β€ π)) β ((π β¨ π) β§ π) β π΄) |
20 | 1, 2, 3, 8, 9, 13, 14, 19 | syl133anc 1393 | 1 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β ((π β¨ π) β§ π) β π΄) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β§ wa 396 β§ w3a 1087 = wceq 1541 β wcel 2106 β wne 2941 class class class wbr 5103 βcfv 6491 (class class class)co 7349 Basecbs 17017 lecple 17074 joincjn 18134 meetcmee 18135 1.cp1 18247 β ccvr 37619 Atomscatm 37620 HLchlt 37707 LHypclh 38342 |
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 5240 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7662 |
This theorem depends on definitions: df-bi 206 df-an 397 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 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5528 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-riota 7305 df-ov 7352 df-oprab 7353 df-proset 18118 df-poset 18136 df-plt 18153 df-lub 18169 df-glb 18170 df-join 18171 df-meet 18172 df-p0 18248 df-p1 18249 df-lat 18255 df-clat 18322 df-oposet 37533 df-ol 37535 df-oml 37536 df-covers 37623 df-ats 37624 df-atl 37655 df-cvlat 37679 df-hlat 37708 df-lhyp 38346 |
This theorem is referenced by: lhpat2 38403 4atexlemex6 38432 trlat 38527 cdlemc5 38553 cdleme3e 38590 cdleme7b 38602 cdleme11k 38626 cdleme16e 38640 cdleme16f 38641 cdlemeda 38656 cdleme22cN 38700 cdleme22d 38701 cdleme23b 38708 cdlemf2 38920 cdlemg12g 39007 cdlemg17dALTN 39022 cdlemg19a 39041 |
Copyright terms: Public domain | W3C validator |