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 syl5eq 
 |-  ( -. 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 syl5eq 
 |-  ( -. 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 ) )