Theorem uvtx2vtx1edgb

Description: If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020)

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

Proof

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