Theorem uvtxel1

Description: Characterization of a universal vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isuvtx.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	uvtxel1	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\leftrightarrow \left(N\in V\wedge \forall k\in \left(V\setminus \left\{N\right\}\right)\exists e\in E\left\{k,N\right\}\subseteq e\right)$$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isuvtx.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		sneq	$$⊢n=N\to \left\{n\right\}=\left\{N\right\}$$
4	3	difeq2d	$$⊢n=N\to V\setminus \left\{n\right\}=V\setminus \left\{N\right\}$$
5		preq2	$$⊢n=N\to \left\{k,n\right\}=\left\{k,N\right\}$$
6	5	sseq1d	$$⊢n=N\to \left(\left\{k,n\right\}\subseteq e\leftrightarrow \left\{k,N\right\}\subseteq e\right)$$
7	6	rexbidv	$$⊢n=N\to \left(\exists e\in E\left\{k,n\right\}\subseteq e\leftrightarrow \exists e\in E\left\{k,N\right\}\subseteq e\right)$$
8	4 7	raleqbidv	$$⊢n=N\to \left(\forall k\in \left(V\setminus \left\{n\right\}\right)\exists e\in E\left\{k,n\right\}\subseteq e\leftrightarrow \forall k\in \left(V\setminus \left\{N\right\}\right)\exists e\in E\left\{k,N\right\}\subseteq e\right)$$
9	1 2	isuvtx	$$⊢\mathrm{UnivVtx}\left(G\right)=\left\{n\in V|\forall k\in \left(V\setminus \left\{n\right\}\right)\exists e\in E\left\{k,n\right\}\subseteq e\right\}$$
10	8 9	elrab2	$$⊢N\in \mathrm{UnivVtx}\left(G\right)\leftrightarrow \left(N\in V\wedge \forall k\in \left(V\setminus \left\{N\right\}\right)\exists e\in E\left\{k,N\right\}\subseteq e\right)$$