Metamath Proof Explorer

Theorem resseqnbas

Description: The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Revised by AV, 19-Oct-2024)

Ref Expression
Hypotheses resseqnbas.r 
|- R = ( W |`s A )
resseqnbas.e 
|- C = ( E ` W )
resseqnbas.f 
|- E = Slot ( E ` ndx )
resseqnbas.n 
|- ( E ` ndx ) =/= ( Base ` ndx )
Assertion resseqnbas 
|- ( A e. V -> C = ( E ` R ) )

Proof

Step Hyp Ref Expression
1 resseqnbas.r 
 |-  R = ( W |`s A )
2 resseqnbas.e 
 |-  C = ( E ` W )
3 resseqnbas.f 
 |-  E = Slot ( E ` ndx )
4 resseqnbas.n 
 |-  ( E ` ndx ) =/= ( Base ` ndx )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 1 5 ressid2 
 |-  ( ( ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> R = W )
7 6 fveq2d 
 |-  ( ( ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
8 7 3expib 
 |-  ( ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
9 1 5 ressval2 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
10 9 fveq2d 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) ) )
11 3 4 setsnid 
 |-  ( E ` W ) = ( E ` ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
12 10 11 eqtr4di 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
13 12 3expib 
 |-  ( -. ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
14 8 13 pm2.61i 
 |-  ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
15 reldmress 
 |-  Rel dom |`s
16 15 ovprc1 
 |-  ( -. W e. _V -> ( W |`s A ) = (/) )
17 1 16 eqtrid 
 |-  ( -. W e. _V -> R = (/) )
18 17 fveq2d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` (/) ) )
19 3 str0 
 |-  (/) = ( E ` (/) )
20 18 19 eqtr4di 
 |-  ( -. W e. _V -> ( E ` R ) = (/) )
21 fvprc 
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
22 20 21 eqtr4d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` W ) )
23 22 adantr 
 |-  ( ( -. W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
24 14 23 pm2.61ian 
 |-  ( A e. V -> ( E ` R ) = ( E ` W ) )
25 2 24 eqtr4id 
 |-  ( A e. V -> C = ( E ` R ) )