Metamath Proof Explorer

Theorem ressinbas

Description: Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 ${⊢}{B}={\mathrm{Base}}_{{W}}$
Assertion ressinbas ${⊢}{A}\in {X}\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$

Proof

Step Hyp Ref Expression
1 ressid.1 ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 elex ${⊢}{A}\in {X}\to {A}\in \mathrm{V}$
3 eqid ${⊢}{W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}{A}$
4 3 1 ressid2 ${⊢}\left({B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}$
5 ssid ${⊢}{B}\subseteq {B}$
6 incom ${⊢}{A}\cap {B}={B}\cap {A}$
7 df-ss ${⊢}{B}\subseteq {A}↔{B}\cap {A}={B}$
8 7 biimpi ${⊢}{B}\subseteq {A}\to {B}\cap {A}={B}$
9 6 8 syl5eq ${⊢}{B}\subseteq {A}\to {A}\cap {B}={B}$
10 5 9 sseqtrrid ${⊢}{B}\subseteq {A}\to {B}\subseteq {A}\cap {B}$
11 elex ${⊢}{W}\in \mathrm{V}\to {W}\in \mathrm{V}$
12 inex1g ${⊢}{A}\in \mathrm{V}\to {A}\cap {B}\in \mathrm{V}$
13 eqid ${⊢}{W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
14 13 1 ressid2 ${⊢}\left({B}\subseteq {A}\cap {B}\wedge {W}\in \mathrm{V}\wedge {A}\cap {B}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}$
15 10 11 12 14 syl3an ${⊢}\left({B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}$
16 4 15 eqtr4d ${⊢}\left({B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
17 16 3expb ${⊢}\left({B}\subseteq {A}\wedge \left({W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
18 inass ${⊢}\left({A}\cap {B}\right)\cap {B}={A}\cap \left({B}\cap {B}\right)$
19 inidm ${⊢}{B}\cap {B}={B}$
20 19 ineq2i ${⊢}{A}\cap \left({B}\cap {B}\right)={A}\cap {B}$
21 18 20 eqtr2i ${⊢}{A}\cap {B}=\left({A}\cap {B}\right)\cap {B}$
22 21 opeq2i ${⊢}⟨{\mathrm{Base}}_{\mathrm{ndx}},{A}\cap {B}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left({A}\cap {B}\right)\cap {B}⟩$
23 22 oveq2i ${⊢}{W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{A}\cap {B}⟩={W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left({A}\cap {B}\right)\cap {B}⟩$
24 3 1 ressval2 ${⊢}\left(¬{B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{A}\cap {B}⟩$
25 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
26 sstr ${⊢}\left({B}\subseteq {A}\cap {B}\wedge {A}\cap {B}\subseteq {A}\right)\to {B}\subseteq {A}$
27 25 26 mpan2 ${⊢}{B}\subseteq {A}\cap {B}\to {B}\subseteq {A}$
28 27 con3i ${⊢}¬{B}\subseteq {A}\to ¬{B}\subseteq {A}\cap {B}$
29 13 1 ressval2 ${⊢}\left(¬{B}\subseteq {A}\cap {B}\wedge {W}\in \mathrm{V}\wedge {A}\cap {B}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left({A}\cap {B}\right)\cap {B}⟩$
30 28 11 12 29 syl3an ${⊢}\left(¬{B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)={W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left({A}\cap {B}\right)\cap {B}⟩$
31 23 24 30 3eqtr4a ${⊢}\left(¬{B}\subseteq {A}\wedge {W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
32 31 3expb ${⊢}\left(¬{B}\subseteq {A}\wedge \left({W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
33 17 32 pm2.61ian ${⊢}\left({W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
34 reldmress ${⊢}\mathrm{Rel}\mathrm{dom}{↾}_{𝑠}$
35 34 ovprc1 ${⊢}¬{W}\in \mathrm{V}\to {W}{↾}_{𝑠}{A}=\varnothing$
36 34 ovprc1 ${⊢}¬{W}\in \mathrm{V}\to {W}{↾}_{𝑠}\left({A}\cap {B}\right)=\varnothing$
37 35 36 eqtr4d ${⊢}¬{W}\in \mathrm{V}\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
38 37 adantr ${⊢}\left(¬{W}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
39 33 38 pm2.61ian ${⊢}{A}\in \mathrm{V}\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$
40 2 39 syl ${⊢}{A}\in {X}\to {W}{↾}_{𝑠}{A}={W}{↾}_{𝑠}\left({A}\cap {B}\right)$