![]() |
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 2797 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | pmapssat.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | pmapssat.m | . . 3 ⊢ 𝑀 = (pmap‘𝐾) | |
5 | 1, 2, 3, 4 | pmapval 35770 | . 2 ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)𝑋}) |
6 | ssrab2 3881 | . 2 ⊢ {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)𝑋} ⊆ 𝐴 | |
7 | 5, 6 | syl6eqss 3849 | 1 ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 {crab 3091 ⊆ wss 3767 class class class wbr 4841 ‘cfv 6099 Basecbs 16181 lecple 16271 Atomscatm 35276 pmapcpmap 35510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-rex 3093 df-reu 3094 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-iun 4710 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-pmap 35517 |
This theorem is referenced by: pmapssbaN 35773 pmapglb2N 35784 pmapglb2xN 35785 pmapjoin 35865 pmapjat1 35866 pmapjat2 35867 pmapjlln1 35868 hlmod1i 35869 polpmapN 35925 2pmaplubN 35939 pmapj2N 35942 pmapocjN 35943 polatN 35944 pmapsubclN 35959 ispsubcl2N 35960 pl42lem2N 35993 pl42lem3N 35994 |
Copyright terms: Public domain | W3C validator |