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 |`s A )
ressbas.b
|- B = ( Base ` W )
Assertion ressbas
|- ( A e. V -> ( A i^i B ) = ( Base ` R ) )

Proof

Step Hyp Ref Expression
1 ressbas.r
 |-  R = ( W |`s A )
2 ressbas.b
 |-  B = ( Base ` W )
3 simp1
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> B C_ A )
4 sseqin2
 |-  ( B C_ A <-> ( A i^i B ) = B )
5 3 4 sylib
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( A i^i B ) = B )
6 1 2 ressid2
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> R = W )
7 6 fveq2d
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( Base ` R ) = ( Base ` W ) )
8 2 5 7 3eqtr4a
 |-  ( ( B C_ A /\ W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) )
9 8 3expib
 |-  ( B C_ A -> ( ( W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) ) )
10 simp2
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> W e. _V )
11 2 fvexi
 |-  B e. _V
12 11 inex2
 |-  ( A i^i B ) e. _V
13 baseid
 |-  Base = Slot ( Base ` ndx )
14 13 setsid
 |-  ( ( W e. _V /\ ( A i^i B ) e. _V ) -> ( A i^i B ) = ( Base ` ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
15 10 12 14 sylancl
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
16 1 2 ressval2
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
17 16 fveq2d
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( Base ` R ) = ( Base ` ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
18 15 17 eqtr4d
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) )
19 18 3expib
 |-  ( -. B C_ A -> ( ( W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) ) )
20 9 19 pm2.61i
 |-  ( ( W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) )
21 0fv
 |-  ( (/) ` ( Base ` ndx ) ) = (/)
22 0ex
 |-  (/) e. _V
23 22 13 strfvn
 |-  ( Base ` (/) ) = ( (/) ` ( Base ` ndx ) )
24 in0
 |-  ( A i^i (/) ) = (/)
25 21 23 24 3eqtr4ri
 |-  ( A i^i (/) ) = ( Base ` (/) )
26 fvprc
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
27 2 26 eqtrid
 |-  ( -. W e. _V -> B = (/) )
28 27 ineq2d
 |-  ( -. W e. _V -> ( A i^i B ) = ( A i^i (/) ) )
29 reldmress
 |-  Rel dom |`s
30 29 ovprc1
 |-  ( -. W e. _V -> ( W |`s A ) = (/) )
31 1 30 eqtrid
 |-  ( -. W e. _V -> R = (/) )
32 31 fveq2d
 |-  ( -. W e. _V -> ( Base ` R ) = ( Base ` (/) ) )
33 25 28 32 3eqtr4a
 |-  ( -. W e. _V -> ( A i^i B ) = ( Base ` R ) )
34 33 adantr
 |-  ( ( -. W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) )
35 20 34 pm2.61ian
 |-  ( A e. V -> ( A i^i B ) = ( Base ` R ) )