Description: The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | cplgr0 | ⊢ ∅ ∈ ComplGraph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ral0 | ⊢ ∀ 𝑣 ∈ ∅ 𝑣 ∈ ( UnivVtx ‘ ∅ ) | |
2 | vtxval0 | ⊢ ( Vtx ‘ ∅ ) = ∅ | |
3 | 2 | raleqi | ⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) ↔ ∀ 𝑣 ∈ ∅ 𝑣 ∈ ( UnivVtx ‘ ∅ ) ) |
4 | 1 3 | mpbir | ⊢ ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) |
5 | 0ex | ⊢ ∅ ∈ V | |
6 | eqid | ⊢ ( Vtx ‘ ∅ ) = ( Vtx ‘ ∅ ) | |
7 | 6 | iscplgr | ⊢ ( ∅ ∈ V → ( ∅ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) ) ) |
8 | 5 7 | ax-mp | ⊢ ( ∅ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ∅ ) 𝑣 ∈ ( UnivVtx ‘ ∅ ) ) |
9 | 4 8 | mpbir | ⊢ ∅ ∈ ComplGraph |