Metamath Proof Explorer

Theorem estrreslem1OLD

Description: Obsolete version of estrreslem1 as of 28-Oct-2024. Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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