Metamath Proof Explorer

Theorem funvtxdmge2val

Description: The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

Ref Expression
Assertion funvtxdmge2val ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → Vtx ⁡ G = Base G

Proof

Step Hyp Ref Expression
1 vtxval ⊢ Vtx ⁡ G = if G ∈ V × V 1 st ⁡ G Base G
2 fundmge2nop0 ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → ¬ G ∈ V × V
3 2 iffalsed ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → if G ∈ V × V 1 st ⁡ G Base G = Base G
4 1 3 syl5eq ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → Vtx ⁡ G = Base G