Metamath Proof Explorer


Theorem estrreslem1

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

Ref Expression
Hypotheses estrres.c φ C = Base ndx B Hom ndx H comp ndx · ˙
estrres.b φ B V
Assertion estrreslem1 φ B = Base C

Proof

Step Hyp Ref Expression
1 estrres.c φ C = Base ndx B Hom ndx H comp ndx · ˙
2 estrres.b φ B V
3 1 fveq2d φ Base C = Base Base ndx B Hom ndx H comp ndx · ˙
4 tpex Base ndx B Hom ndx H comp ndx · ˙ V
5 4 a1i φ Base ndx B Hom ndx H comp ndx · ˙ V
6 df-base Base = Slot 1
7 1nn 1
8 5 6 7 strndxid φ Base ndx B Hom ndx H comp ndx · ˙ Base ndx = Base Base ndx B Hom ndx H comp ndx · ˙
9 fvexd φ Base ndx 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 φ Base ndx Hom ndx Base ndx comp ndx
13 fvtp1g Base ndx V B V Base ndx Hom ndx Base ndx comp ndx Base ndx B Hom ndx H comp ndx · ˙ Base ndx = B
14 9 2 12 13 syl21anc φ Base ndx B Hom ndx H comp ndx · ˙ Base ndx = B
15 3 8 14 3eqtr2rd φ B = Base C