Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | usgr0eop | ⊢ ( 𝑉 ∈ 𝑊 → 〈 𝑉 , ∅ 〉 ∈ USGraph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opex | ⊢ 〈 𝑉 , ∅ 〉 ∈ V | |
2 | 1 | a1i | ⊢ ( 𝑉 ∈ 𝑊 → 〈 𝑉 , ∅ 〉 ∈ V ) |
3 | 0ex | ⊢ ∅ ∈ V | |
4 | opiedgfv | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∅ ∈ V ) → ( iEdg ‘ 〈 𝑉 , ∅ 〉 ) = ∅ ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝑉 ∈ 𝑊 → ( iEdg ‘ 〈 𝑉 , ∅ 〉 ) = ∅ ) |
6 | 2 5 | usgr0e | ⊢ ( 𝑉 ∈ 𝑊 → 〈 𝑉 , ∅ 〉 ∈ USGraph ) |