# Metamath Proof Explorer

## Theorem ressbas

Description: Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014)

Ref Expression
Hypotheses ressbas.r $⊢ R = W ↾ 𝑠 A$
ressbas.b $⊢ B = Base W$
Assertion ressbas $⊢ A ∈ V → A ∩ B = Base R$

### Proof

Step Hyp Ref Expression
1 ressbas.r $⊢ R = W ↾ 𝑠 A$
2 ressbas.b $⊢ B = Base W$
3 simp1 $⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → B ⊆ A$
4 sseqin2 $⊢ B ⊆ A ↔ A ∩ B = B$
5 3 4 sylib $⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → A ∩ B = B$
6 1 2 ressid2 $⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → R = W$
7 6 fveq2d $⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → Base R = Base W$
8 2 5 7 3eqtr4a $⊢ B ⊆ A ∧ W ∈ V ∧ A ∈ V → A ∩ B = Base R$
9 8 3expib $⊢ B ⊆ A → W ∈ V ∧ A ∈ V → A ∩ B = Base R$
10 simp2 $⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → W ∈ V$
11 2 fvexi $⊢ B ∈ V$
12 11 inex2 $⊢ A ∩ B ∈ V$
13 baseid $⊢ Base = Slot Base ndx$
14 13 setsid $⊢ W ∈ V ∧ A ∩ B ∈ V → A ∩ B = Base W sSet Base ndx A ∩ B$
15 10 12 14 sylancl $⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → A ∩ B = Base W sSet Base ndx A ∩ B$
16 1 2 ressval2 $⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → R = W sSet Base ndx A ∩ B$
17 16 fveq2d $⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → Base R = Base W sSet Base ndx A ∩ B$
18 15 17 eqtr4d $⊢ ¬ B ⊆ A ∧ W ∈ V ∧ A ∈ V → A ∩ B = Base R$
19 18 3expib $⊢ ¬ B ⊆ A → W ∈ V ∧ A ∈ V → A ∩ B = Base R$
20 9 19 pm2.61i $⊢ W ∈ V ∧ A ∈ V → A ∩ B = Base R$
21 0fv $⊢ ∅ ⁡ Base ndx = ∅$
22 0ex $⊢ ∅ ∈ V$
23 22 13 strfvn $⊢ Base ∅ = ∅ ⁡ Base ndx$
24 in0 $⊢ A ∩ ∅ = ∅$
25 21 23 24 3eqtr4ri $⊢ A ∩ ∅ = Base ∅$
26 fvprc $⊢ ¬ W ∈ V → Base W = ∅$
27 2 26 syl5eq $⊢ ¬ W ∈ V → B = ∅$
28 27 ineq2d $⊢ ¬ W ∈ V → A ∩ B = A ∩ ∅$
29 reldmress $⊢ Rel ⁡ dom ⁡ ↾ 𝑠$
30 29 ovprc1 $⊢ ¬ W ∈ V → W ↾ 𝑠 A = ∅$
31 1 30 syl5eq $⊢ ¬ W ∈ V → R = ∅$
32 31 fveq2d $⊢ ¬ W ∈ V → Base R = Base ∅$
33 25 28 32 3eqtr4a $⊢ ¬ W ∈ V → A ∩ B = Base R$
34 33 adantr $⊢ ¬ W ∈ V ∧ A ∈ V → A ∩ B = Base R$
35 20 34 pm2.61ian $⊢ A ∈ V → A ∩ B = Base R$