Metamath Proof Explorer

Theorem funvtxdm2val

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

Ref Expression
Hypotheses funvtxdm2val.a ⊢ A ∈ V
funvtxdm2val.b ⊢ B ∈ V
Assertion funvtxdm2val ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → Vtx ⁡ G = Base G

Proof

Step Hyp Ref Expression
1 funvtxdm2val.a ⊢ A ∈ V
2 funvtxdm2val.b ⊢ B ∈ V
3 vtxval ⊢ Vtx ⁡ G = if G ∈ V × V 1 st ⁡ G Base G
4 1 2 fun2dmnop0 ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → ¬ G ∈ V × V
5 4 iffalsed ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → if G ∈ V × V 1 st ⁡ G Base G = Base G
6 3 5 syl5eq ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → Vtx ⁡ G = Base G