Metamath Proof Explorer

Theorem cplgr2v

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020)

Ref Expression
Hypotheses cplgr0v.v ⊢V=Vtx⁡G
cplgr2v.e ⊢E=Edg⁡G
Assertion cplgr2v ⊢G∈UHGraph∧V=2→G∈ComplGraph↔V∈E

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢V=Vtx⁡G
2 cplgr2v.e ⊢E=Edg⁡G
3 1 iscplgr ⊢G∈UHGraph→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
4 3 adantr ⊢G∈UHGraph∧V=2→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
5 1 2 uvtx2vtx1edgb ⊢G∈UHGraph∧V=2→V∈E↔∀v∈Vv∈UnivVtx⁡G
6 4 5 bitr4d ⊢G∈UHGraph∧V=2→G∈ComplGraph↔V∈E