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

Metamath Proof Explorer

Theorem setsvtx

Description: The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses setsvtx.i ⊢ I = ef ⁡ ndx
setsvtx.s ⊢ φ → G Struct X
setsvtx.b ⊢ φ → Base ndx ∈ dom ⁡ G
setsvtx.e ⊢ φ → E ∈ W
Assertion setsvtx ⊢ φ → Vtx ⁡ G sSet I E = Base G

Proof

Step Hyp Ref Expression
1 setsvtx.i ⊢ I = ef ⁡ ndx
2 setsvtx.s ⊢ φ → G Struct X
3 setsvtx.b ⊢ φ → Base ndx ∈ dom ⁡ G
4 setsvtx.e ⊢ φ → E ∈ W
5 1 fvexi ⊢ I ∈ V
6 5 a1i ⊢ φ → I ∈ V
7 2 6 4 setsn0fun ⊢ φ → Fun ⁡ G sSet I E ∖ ∅
8 1 eqcomi ⊢ ef ⁡ ndx = I
9 8 preq2i ⊢ Base ndx ef ⁡ ndx = Base ndx I
10 2 6 4 3 basprssdmsets ⊢ φ → Base ndx I ⊆ dom ⁡ G sSet I E
11 9 10 eqsstrid ⊢ φ → Base ndx ef ⁡ ndx ⊆ dom ⁡ G sSet I E
12 funvtxval ⊢ Fun ⁡ G sSet I E ∖ ∅ ∧ Base ndx ef ⁡ ndx ⊆ dom ⁡ G sSet I E → Vtx ⁡ G sSet I E = Base G sSet I E
13 7 11 12 syl2anc ⊢ φ → Vtx ⁡ G sSet I E = Base G sSet I E
14 baseid ⊢ Base = Slot Base ndx
15 basendxnedgfndx ⊢ Base ndx ≠ ef ⁡ ndx
16 15 1 neeqtrri ⊢ Base ndx ≠ I
17 14 16 setsnid ⊢ Base G = Base G sSet I E
18 13 17 eqtr4di ⊢ φ → Vtx ⁡ G sSet I E = Base G