![]() |
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 1116 | . . . . . 6 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐵 ⊆ 𝐴) | |
3 | sseqin2 4073 | . . . . . 6 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 𝐵) | |
4 | 2, 3 | sylib 210 | . . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = 𝐵) |
5 | ressbas.r | . . . . . . 7 ⊢ 𝑅 = (𝑊 ↾s 𝐴) | |
6 | 5, 1 | ressid2 16402 | . . . . . 6 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑊) |
7 | 6 | fveq2d 6497 | . . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Base‘𝑅) = (Base‘𝑊)) |
8 | 1, 4, 7 | 3eqtr4a 2834 | . . . 4 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
9 | 8 | 3expib 1102 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅))) |
10 | simp2 1117 | . . . . . 6 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑊 ∈ V) | |
11 | 1 | fvexi 6507 | . . . . . . 7 ⊢ 𝐵 ∈ V |
12 | 11 | inex2 5073 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ∈ V |
13 | baseid 16393 | . . . . . . 7 ⊢ Base = Slot (Base‘ndx) | |
14 | 13 | setsid 16388 | . . . . . 6 ⊢ ((𝑊 ∈ V ∧ (𝐴 ∩ 𝐵) ∈ V) → (𝐴 ∩ 𝐵) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
15 | 10, 12, 14 | sylancl 577 | . . . . 5 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
16 | 5, 1 | ressval2 16403 | . . . . . 6 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
17 | 16 | fveq2d 6497 | . . . . 5 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (Base‘𝑅) = (Base‘(𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
18 | 15, 17 | eqtr4d 2811 | . . . 4 ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
19 | 18 | 3expib 1102 | . . 3 ⊢ (¬ 𝐵 ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅))) |
20 | 9, 19 | pm2.61i 177 | . 2 ⊢ ((𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
21 | 0fv 6533 | . . . . 5 ⊢ (∅‘(Base‘ndx)) = ∅ | |
22 | 0ex 5062 | . . . . . 6 ⊢ ∅ ∈ V | |
23 | 22, 13 | strfvn 16355 | . . . . 5 ⊢ (Base‘∅) = (∅‘(Base‘ndx)) |
24 | in0 4225 | . . . . 5 ⊢ (𝐴 ∩ ∅) = ∅ | |
25 | 21, 23, 24 | 3eqtr4ri 2807 | . . . 4 ⊢ (𝐴 ∩ ∅) = (Base‘∅) |
26 | fvprc 6486 | . . . . . 6 ⊢ (¬ 𝑊 ∈ V → (Base‘𝑊) = ∅) | |
27 | 1, 26 | syl5eq 2820 | . . . . 5 ⊢ (¬ 𝑊 ∈ V → 𝐵 = ∅) |
28 | 27 | ineq2d 4070 | . . . 4 ⊢ (¬ 𝑊 ∈ V → (𝐴 ∩ 𝐵) = (𝐴 ∩ ∅)) |
29 | reldmress 16400 | . . . . . . 7 ⊢ Rel dom ↾s | |
30 | 29 | ovprc1 7008 | . . . . . 6 ⊢ (¬ 𝑊 ∈ V → (𝑊 ↾s 𝐴) = ∅) |
31 | 5, 30 | syl5eq 2820 | . . . . 5 ⊢ (¬ 𝑊 ∈ V → 𝑅 = ∅) |
32 | 31 | fveq2d 6497 | . . . 4 ⊢ (¬ 𝑊 ∈ V → (Base‘𝑅) = (Base‘∅)) |
33 | 25, 28, 32 | 3eqtr4a 2834 | . . 3 ⊢ (¬ 𝑊 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
34 | 33 | adantr 473 | . 2 ⊢ ((¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
35 | 20, 34 | pm2.61ian 799 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 Vcvv 3409 ∩ cin 3822 ⊆ wss 3823 ∅c0 4172 〈cop 4441 ‘cfv 6182 (class class class)co 6970 ndxcnx 16330 sSet csts 16331 Basecbs 16333 ↾s cress 16334 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-1cn 10387 ax-addcl 10389 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-nn 11434 df-ndx 16336 df-slot 16337 df-base 16339 df-sets 16340 df-ress 16341 |
This theorem is referenced by: ressbas2 16405 ressbasss 16406 ressress 16412 rescabs 16955 resscatc 17217 resscntz 18227 idrespermg 18294 opprsubg 19103 subrgpropd 19286 sralmod 19675 resstopn 21492 resstps 21493 ressuss 22569 ressxms 22832 ressms 22833 cphsubrglem 23478 cphsscph 23551 resspos 30378 resstos 30379 xrge0base 30404 xrge00 30405 submomnd 30429 suborng 30567 gsumge0cl 42084 sge0tsms 42093 lidlssbas 43557 lidlbas 43558 uzlidlring 43564 dmatALTbas 43823 |
Copyright terms: Public domain | W3C validator |