Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Complete graphs
iscplgr
Next ⟩
iscplgrnb
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscplgr
Description:
The property of being a complete graph.
(Contributed by
AV
, 1-Nov-2020)
Ref
Expression
Hypothesis
cplgruvtxb.v
⊢
V
=
Vtx
⁡
G
Assertion
iscplgr
⊢
G
∈
W
→
G
∈
ComplGraph
↔
∀
v
∈
V
v
∈
UnivVtx
⁡
G
Proof
Step
Hyp
Ref
Expression
1
cplgruvtxb.v
⊢
V
=
Vtx
⁡
G
2
1
cplgruvtxb
⊢
G
∈
W
→
G
∈
ComplGraph
↔
UnivVtx
⁡
G
=
V
3
eqss
⊢
UnivVtx
⁡
G
=
V
↔
UnivVtx
⁡
G
⊆
V
∧
V
⊆
UnivVtx
⁡
G
4
1
uvtxssvtx
⊢
UnivVtx
⁡
G
⊆
V
5
dfss3
⊢
V
⊆
UnivVtx
⁡
G
↔
∀
v
∈
V
v
∈
UnivVtx
⁡
G
6
5
anbi2i
⊢
UnivVtx
⁡
G
⊆
V
∧
V
⊆
UnivVtx
⁡
G
↔
UnivVtx
⁡
G
⊆
V
∧
∀
v
∈
V
v
∈
UnivVtx
⁡
G
7
4
6
mpbiran
⊢
UnivVtx
⁡
G
⊆
V
∧
V
⊆
UnivVtx
⁡
G
↔
∀
v
∈
V
v
∈
UnivVtx
⁡
G
8
3
7
bitri
⊢
UnivVtx
⁡
G
=
V
↔
∀
v
∈
V
v
∈
UnivVtx
⁡
G
9
2
8
syl6bb
⊢
G
∈
W
→
G
∈
ComplGraph
↔
∀
v
∈
V
v
∈
UnivVtx
⁡
G