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

Metamath Proof Explorer

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 ‘ 𝐺 ) ) )