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

Metamath Proof Explorer

Theorem uvtx2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

		Ref	Expression
	Hypotheses	uvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
		isuvtx.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	Assertion	uvtx2vtx1edg	⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isuvtx.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	nbgr2vtx1edg	⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
4	1	uvtxel	⊢ ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
5	4	a1i	⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
6	5	baibd	⊢ ( ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
7	6	ralbidva	⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ( ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
8	3 7	mpbird	⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )