Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > pmapssat | Structured version Visualization version GIF version |
Description: The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
Ref | Expression |
---|---|
pmapssat.b | ⊢ 𝐵 = (Base‘𝐾) |
pmapssat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
pmapssat.m | ⊢ 𝑀 = (pmap‘𝐾) |
Ref | Expression |
---|---|
pmapssat | ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmapssat.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
2 | eqid 2737 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | pmapssat.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | pmapssat.m | . . 3 ⊢ 𝑀 = (pmap‘𝐾) | |
5 | 1, 2, 3, 4 | pmapval 37740 | . 2 ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)𝑋}) |
6 | ssrab2 4014 | . 2 ⊢ {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)𝑋} ⊆ 𝐴 | |
7 | 5, 6 | eqsstrdi 3976 | 1 ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 {crab 3066 ⊆ wss 3888 class class class wbr 5075 ‘cfv 6423 Basecbs 16856 lecple 16913 Atomscatm 37246 pmapcpmap 37480 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 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 2708 ax-rep 5210 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3429 df-sbc 3717 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4259 df-if 4462 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-iun 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5485 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-iota 6381 df-fun 6425 df-fn 6426 df-f 6427 df-f1 6428 df-fo 6429 df-f1o 6430 df-fv 6431 df-pmap 37487 |
This theorem is referenced by: pmapssbaN 37743 pmapglb2N 37754 pmapglb2xN 37755 pmapjoin 37835 pmapjat1 37836 pmapjat2 37837 pmapjlln1 37838 hlmod1i 37839 polpmapN 37895 2pmaplubN 37909 pmapj2N 37912 pmapocjN 37913 polatN 37914 pmapsubclN 37929 ispsubcl2N 37930 pl42lem2N 37963 pl42lem3N 37964 |
Copyright terms: Public domain | W3C validator |