Metamath Proof Explorer

Theorem ressbas

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

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 in0 
 |-  ( A i^i (/) ) = (/)
22 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
23 2 22 eqtrid 
 |-  ( -. W e. _V -> B = (/) )
24 23 ineq2d 
 |-  ( -. W e. _V -> ( A i^i B ) = ( A i^i (/) ) )
25 21 24 22 3eqtr4a 
 |-  ( -. W e. _V -> ( A i^i B ) = ( Base ` W ) )
26 base0 
 |-  (/) = ( Base ` (/) )
27 26 eqcomi 
 |-  ( Base ` (/) ) = (/)
28 reldmress 
 |-  Rel dom |`s
29 27 1 28 oveqprc 
 |-  ( -. W e. _V -> ( Base ` W ) = ( Base ` R ) )
30 25 29 eqtrd 
 |-  ( -. W e. _V -> ( A i^i B ) = ( Base ` R ) )
31 30 adantr 
 |-  ( ( -. W e. _V /\ A e. V ) -> ( A i^i B ) = ( Base ` R ) )
32 20 31 pm2.61ian 
 |-  ( A e. V -> ( A i^i B ) = ( Base ` R ) )