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	3	str0	|- (/) = ( E ` (/) )
16	15	eqcomi	|- ( E ` (/) ) = (/)
17		reldmress	|- Rel dom |`s
18	16 1 17	oveqprc	|- ( -. W e. _V -> ( E ` W ) = ( E ` R ) )
19	18	eqcomd	|- ( -. W e. _V -> ( E ` R ) = ( E ` W ) )
20	19	adantr	|- ( ( -. W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
21	14 20	pm2.61ian	|- ( A e. V -> ( E ` R ) = ( E ` W ) )
22	2 21	eqtr4id	|- ( A e. V -> C = ( E ` R ) )