# Metamath Proof Explorer

## Theorem estrreslem1

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

Ref Expression
Hypotheses estrres.c ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
estrres.b ( 𝜑𝐵𝑉 )
Assertion estrreslem1 ( 𝜑𝐵 = ( Base ‘ 𝐶 ) )

### Proof

Step Hyp Ref Expression
1 estrres.c ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
2 estrres.b ( 𝜑𝐵𝑉 )
3 1 fveq2d ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ) )
4 tpex { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
5 4 a1i ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
6 df-base Base = Slot 1
7 1nn 1 ∈ ℕ
8 5 6 7 strndxid ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( 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 ∧ 𝐵𝑉 ) ∧ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
14 9 2 12 13 syl21anc ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
15 3 8 14 3eqtr2rd ( 𝜑𝐵 = ( Base ‘ 𝐶 ) )