This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelstrbas

Description: The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021)

Ref Expression
Hypotheses opelstrbas.s ⊢ φ → S Struct X
opelstrbas.v ⊢ φ → V ∈ Y
opelstrbas.b ⊢ φ → Base ndx V ∈ S
Assertion opelstrbas ⊢ φ → V = Base S

Proof

Step Hyp Ref Expression
1 opelstrbas.s ⊢ φ → S Struct X
2 opelstrbas.v ⊢ φ → V ∈ Y
3 opelstrbas.b ⊢ φ → Base ndx V ∈ S
4 baseid ⊢ Base = Slot Base ndx
5 structex ⊢ S Struct X → S ∈ V
6 1 5 syl ⊢ φ → S ∈ V
7 structfung ⊢ S Struct X → Fun ⁡ S -1 -1
8 1 7 syl ⊢ φ → Fun ⁡ S -1 -1
9 4 6 8 3 2 strfv2d ⊢ φ → V = Base S