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 ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 vtxval ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1st𝐺 ) , ( Base ‘ 𝐺 ) )
2 fundmge2nop0 ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )
3 2 iffalsed ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → if ( 𝐺 ∈ ( V × V ) , ( 1st𝐺 ) , ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐺 ) )
4 1 3 syl5eq ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )