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

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 \in V$
		funvtxdm2val.b	$⊢ B \in V$
	Assertion	funvtxdm2val	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to Vtx (G) = {Base}_{G}$

Proof

Step	Hyp	Ref	Expression
1		funvtxdm2val.a	$⊢ A \in V$
2		funvtxdm2val.b	$⊢ B \in V$
3		vtxval	$⊢ Vtx (G) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$
4	1 2	fun2dmnop0	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to \neg G \in (V \times V)$
5	4	iffalsed	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to if (G \in (V \times V), 1^{st} (G), {Base}_{G}) = {Base}_{G}$
6	3 5	eqtrid	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to Vtx (G) = {Base}_{G}$