![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ressbas | Structured version Visualization version GIF version |
Description: Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) |
Ref | Expression |
---|---|
ressbas.r | ⊢ 𝑅 = (𝑊 ↾s 𝐴) |
ressbas.b | ⊢ 𝐵 = (Base‘𝑊) |
Ref | Expression |
---|---|
ressbas | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressbas.b | . . . . 5 ⊢ 𝐵 = (Base‘𝑊) | |
2 | simp1 1131 | . . . . . 6 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐵 ⊆ 𝐴) | |
3 | sseqin2 3958 | . . . . . 6 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 𝐵) | |
4 | 2, 3 | sylib 208 | . . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = 𝐵) |
5 | ressbas.r | . . . . . . 7 ⊢ 𝑅 = (𝑊 ↾s 𝐴) | |
6 | 5, 1 | ressid2 16128 | . . . . . 6 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑊) |
7 | 6 | fveq2d 6354 | . . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Base‘𝑅) = (Base‘𝑊)) |
8 | 1, 4, 7 | 3eqtr4a 2818 | . . . 4 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
9 | 8 | 3expib 1117 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅))) |
10 | simp2 1132 | . . . . . 6 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑊 ∈ V) | |
11 | fvex 6360 | . . . . . . . 8 ⊢ (Base‘𝑊) ∈ V | |
12 | 1, 11 | eqeltri 2833 | . . . . . . 7 ⊢ 𝐵 ∈ V |
13 | 12 | inex2 4950 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ∈ V |
14 | baseid 16119 | . . . . . . 7 ⊢ Base = Slot (Base‘ndx) | |
15 | 14 | setsid 16114 | . . . . . 6 ⊢ ((𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝐴 ∩ 𝐵) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
16 | 10, 13, 15 | sylancl 697 | . . . . 5 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
17 | 5, 1 | ressval2 16129 | . . . . . 6 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
18 | 17 | fveq2d 6354 | . . . . 5 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Base‘𝑅) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
19 | 16, 18 | eqtr4d 2795 | . . . 4 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
20 | 19 | 3expib 1117 | . . 3 ⊢ (¬ 𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅))) |
21 | 9, 20 | pm2.61i 176 | . 2 ⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
22 | 0fv 6386 | . . . . 5 ⊢ (∅‘(Base‘ndx)) = ∅ | |
23 | 0ex 4940 | . . . . . 6 ⊢ ∅ ∈ V | |
24 | 23, 14 | strfvn 16079 | . . . . 5 ⊢ (Base‘∅) = (∅‘(Base‘ndx)) |
25 | in0 4109 | . . . . 5 ⊢ (𝐴 ∩ ∅) = ∅ | |
26 | 22, 24, 25 | 3eqtr4ri 2791 | . . . 4 ⊢ (𝐴 ∩ ∅) = (Base‘∅) |
27 | fvprc 6344 | . . . . . 6 ⊢ (¬ 𝑊 ∈ V → (Base‘𝑊) = ∅) | |
28 | 1, 27 | syl5eq 2804 | . . . . 5 ⊢ (¬ 𝑊 ∈ V → 𝐵 = ∅) |
29 | 28 | ineq2d 3955 | . . . 4 ⊢ (¬ 𝑊 ∈ V → (𝐴 ∩ 𝐵) = (𝐴 ∩ ∅)) |
30 | reldmress 16126 | . . . . . . 7 ⊢ Rel dom ↾s | |
31 | 30 | ovprc1 6845 | . . . . . 6 ⊢ (¬ 𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
32 | 5, 31 | syl5eq 2804 | . . . . 5 ⊢ (¬ 𝑊 ∈ V → 𝑅 = ∅) |
33 | 32 | fveq2d 6354 | . . . 4 ⊢ (¬ 𝑊 ∈ V → (Base‘𝑅) = (Base‘∅)) |
34 | 26, 29, 33 | 3eqtr4a 2818 | . . 3 ⊢ (¬ 𝑊 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
35 | 34 | adantr 472 | . 2 ⊢ ((¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
36 | 21, 35 | pm2.61ian 866 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1630 ∈ wcel 2137 Vcvv 3338 ∩ cin 3712 ⊆ wss 3713 ∅c0 4056 〈cop 4325 ‘cfv 6047 (class class class)co 6811 ndxcnx 16054 sSet csts 16055 Basecbs 16057 ↾s cress 16058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-cnex 10182 ax-resscn 10183 ax-1cn 10184 ax-icn 10185 ax-addcl 10186 ax-addrcl 10187 ax-mulcl 10188 ax-mulrcl 10189 ax-i2m1 10194 ax-1ne0 10195 ax-rrecex 10198 ax-cnre 10199 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-ral 3053 df-rex 3054 df-reu 3055 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-pss 3729 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-tp 4324 df-op 4326 df-uni 4587 df-iun 4672 df-br 4803 df-opab 4863 df-mpt 4880 df-tr 4903 df-id 5172 df-eprel 5177 df-po 5185 df-so 5186 df-fr 5223 df-we 5225 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-pred 5839 df-ord 5885 df-on 5886 df-lim 5887 df-suc 5888 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-f1 6052 df-fo 6053 df-f1o 6054 df-fv 6055 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-om 7229 df-wrecs 7574 df-recs 7635 df-rdg 7673 df-nn 11211 df-ndx 16060 df-slot 16061 df-base 16063 df-sets 16064 df-ress 16065 |
This theorem is referenced by: ressbas2 16131 ressbasss 16132 ressress 16138 rescabs 16692 resscatc 16954 resscntz 17962 idrespermg 18029 opprsubg 18834 subrgpropd 19014 sralmod 19387 resstopn 21190 resstps 21191 ressuss 22266 ressxms 22529 ressms 22530 cphsubrglem 23175 resspos 29966 resstos 29967 xrge0base 29992 xrge00 29993 submomnd 30017 suborng 30122 gsumge0cl 41089 sge0tsms 41098 lidlssbas 42430 lidlbas 42431 uzlidlring 42437 dmatALTbas 42698 |
Copyright terms: Public domain | W3C validator |