Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > polssatN | Structured version Visualization version GIF version |
Description: The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
Ref | Expression |
---|---|
polssat.a | β’ π΄ = (AtomsβπΎ) |
polssat.p | β’ β₯ = (β₯πβπΎ) |
Ref | Expression |
---|---|
polssatN | β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | polssat.a | . . 3 β’ π΄ = (AtomsβπΎ) | |
2 | eqid 2736 | . . 3 β’ (PSubSpβπΎ) = (PSubSpβπΎ) | |
3 | polssat.p | . . 3 β’ β₯ = (β₯πβπΎ) | |
4 | 1, 2, 3 | polsubN 38183 | . 2 β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β (PSubSpβπΎ)) |
5 | 1, 2 | psubssat 38030 | . 2 β’ ((πΎ β HL β§ ( β₯ βπ) β (PSubSpβπΎ)) β ( β₯ βπ) β π΄) |
6 | 4, 5 | syldan 591 | 1 β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 396 = wceq 1540 β wcel 2105 β wss 3898 βcfv 6479 Atomscatm 37538 HLchlt 37625 PSubSpcpsubsp 37772 β₯πcpolN 38178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-riota 7293 df-ov 7340 df-oprab 7341 df-proset 18110 df-poset 18128 df-lub 18161 df-glb 18162 df-join 18163 df-meet 18164 df-p1 18241 df-lat 18247 df-clat 18314 df-oposet 37451 df-ol 37453 df-oml 37454 df-ats 37542 df-atl 37573 df-cvlat 37597 df-hlat 37626 df-psubsp 37779 df-pmap 37780 df-polarityN 38179 |
This theorem is referenced by: 2polcon4bN 38194 polcon2N 38195 pclss2polN 38197 2pmaplubN 38202 paddunN 38203 ispsubcl2N 38223 poml5N 38230 osumcllem1N 38232 osumcllem2N 38233 osumcllem3N 38234 osumcllem9N 38240 osumcllem11N 38242 pexmidN 38245 pexmidlem2N 38247 pexmidlem3N 38248 pexmidlem7N 38252 pexmidlem8N 38253 |
Copyright terms: Public domain | W3C validator |