Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ressbas2 | Structured version Visualization version GIF version |
Description: Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
ressbas.r | ⊢ 𝑅 = (𝑊 ↾s 𝐴) |
ressbas.b | ⊢ 𝐵 = (Base‘𝑊) |
Ref | Expression |
---|---|
ressbas2 | ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ss 3952 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
2 | 1 | biimpi 218 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴) |
3 | ressbas.b | . . . . 5 ⊢ 𝐵 = (Base‘𝑊) | |
4 | 3 | fvexi 6684 | . . . 4 ⊢ 𝐵 ∈ V |
5 | 4 | ssex 5225 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
6 | ressbas.r | . . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴) | |
7 | 6, 3 | ressbas 16554 | . . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
8 | 5, 7 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
9 | 2, 8 | eqtr3d 2858 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 Vcvv 3494 ∩ cin 3935 ⊆ wss 3936 ‘cfv 6355 (class class class)co 7156 Basecbs 16483 ↾s cress 16484 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-1cn 10595 ax-addcl 10597 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-nn 11639 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 |
This theorem is referenced by: rescbas 17099 fullresc 17121 resssetc 17352 yoniso 17535 issstrmgm 17863 gsumress 17892 issubmnd 17938 ress0g 17939 submnd0 17940 submbas 17979 resmhm 17985 resgrpplusfrn 18117 subgbas 18283 issubg2 18294 resghm 18374 symgbas 18499 submod 18694 cntrcmnd 18962 ringidss 19327 unitgrpbas 19416 isdrng2 19512 drngmcl 19515 drngid2 19518 isdrngd 19527 cntzsdrg 19581 subdrgint 19582 primefld 19584 islss3 19731 lsslss 19733 lsslsp 19787 reslmhm 19824 resspsrbas 20195 mplbas 20209 ressmplbas 20237 evlssca 20302 mpfconst 20314 mpfind 20320 ply1bas 20363 ressply1bas 20397 evls1sca 20486 xrs1mnd 20583 xrs10 20584 xrs1cmn 20585 xrge0subm 20586 xrge0cmn 20587 cnmsubglem 20608 nn0srg 20615 rge0srg 20616 zringbas 20623 expghm 20643 cnmsgnbas 20722 psgnghm 20724 rebase 20750 dsmmbase 20879 dsmmval2 20880 lsslindf 20974 lsslinds 20975 islinds3 20978 m2cpmrngiso 21366 ressusp 22874 imasdsf1olem 22983 xrge0gsumle 23441 xrge0tsms 23442 cmssmscld 23953 cmsss 23954 minveclem3a 24030 efabl 25134 efsubm 25135 qrngbas 26195 ressplusf 30637 ressnm 30638 ressprs 30642 ressmulgnn 30670 ressmulgnn0 30671 xrge0tsmsd 30692 ress1r 30860 xrge0slmod 30917 drgextlsp 30996 lssdimle 31006 lbslsat 31014 dimkerim 31023 fedgmullem1 31025 fedgmullem2 31026 fedgmul 31027 prsssdm 31160 ordtrestNEW 31164 ordtrest2NEW 31166 xrge0iifmhm 31182 esumpfinvallem 31333 sitgaddlemb 31606 prdsbnd2 35088 cnpwstotbnd 35090 repwsmet 35127 rrnequiv 35128 lcdvbase 38744 selvval2lem4 39185 islssfg 39719 lnmlsslnm 39730 pwssplit4 39738 deg1mhm 39856 gsumge0cl 42702 sge0tsms 42711 cnfldsrngbas 44085 issubmgm2 44106 submgmbas 44112 resmgmhm 44114 amgmlemALT 44953 |
Copyright terms: Public domain | W3C validator |