# Metamath Proof Explorer

## 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 ) )`