This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem estrreslem1

Description: Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020) (Proof shortened by AV, 28-Oct-2024)

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 baseid 
 |-  Base = Slot ( Base ` ndx )
5 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
6 5 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V )
7 4 6 strfvnd 
 |-  ( ph -> ( Base ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ` ( Base ` ndx ) ) )
8 fvexd 
 |-  ( ph -> ( Base ` ndx ) e. _V )
9 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
10 3simpa 
 |-  ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) ) )
11 9 10 mp1i 
 |-  ( ph -> ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) ) )
12 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 )
13 8 2 11 12 syl21anc 
 |-  ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ` ( Base ` ndx ) ) = B )
14 3 7 13 3eqtrrd 
 |-  ( ph -> B = ( Base ` C ) )