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 ⊢ ( 𝜑 → 𝐶 = { ⟨ ( 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 baseid ⊢ Base = Slot ( Base ‘ ndx )
5 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
6 5 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V )
7 4 6 strfvnd ⊢ ( 𝜑 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) )
8 fvexd ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 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 ⊢ ( 𝜑 → ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) )
12 fvtp1g ⊢ ( ( ( ( Base ‘ ndx ) ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
13 8 2 11 12 syl21anc ⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ‘ ( Base ‘ ndx ) ) = 𝐵 )
14 3 7 13 3eqtrrd ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )