Theorem estrreslem1

Description: Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020)

	Ref	Expression
Hypotheses	estrres.c	|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
	estrres.b	|- ( ph -> B e. V )
Assertion	estrreslem1	|- ( ph -> B = ( Base ` C ) )

Proof

Step	Hyp	Ref	Expression
1		estrres.c	|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
2		estrres.b	|- ( ph -> B e. V )
3	1	fveq2d	|- ( ph -> ( Base ` C ) = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) )
4		tpex	|- { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
5	4	a1i	|- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V )
6		df-base	|- Base = Slot 1
7		1nn	|- 1 e. NN
8	5 6 7	strndxid	|- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ` ( Base ` ndx ) ) = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) )
9		fvexd	|- ( ph -> ( Base ` ndx ) e. _V )
10		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
11		3simpa	|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) ) )
12	10 11	mp1i	|- ( ph -> ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) ) )
13		fvtp1g	|- ( ( ( ( Base ` ndx ) e. _V /\ B e. V ) /\ ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) ) ) -> ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ` ( Base ` ndx ) ) = B )
14	9 2 12 13	syl21anc	|- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ` ( Base ` ndx ) ) = B )
15	3 8 14	3eqtr2rd	|- ( ph -> B = ( Base ` C ) )