# Metamath Proof Explorer

## Theorem estrreslem1

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

Ref Expression
Hypotheses estrres.c
estrres.b ${⊢}{\phi }\to {B}\in {V}$
Assertion estrreslem1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$

### Proof

Step Hyp Ref Expression
1 estrres.c
2 estrres.b ${⊢}{\phi }\to {B}\in {V}$
3 1 fveq2d
4 tpex
5 4 a1i
6 df-base ${⊢}\mathrm{Base}=\mathrm{Slot}1$
7 1nn ${⊢}1\in ℕ$
8 5 6 7 strndxid
9 fvexd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
10 slotsbhcdif ${⊢}\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$
11 3simpa ${⊢}\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$
12 10 11 mp1i ${⊢}{\phi }\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$
13 fvtp1g
14 9 2 12 13 syl21anc
15 3 8 14 3eqtr2rd ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$