Description: A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020) (Proof shortened by AV, 8-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | uhgriedg0edg0 | ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) | |
2 | 1 | uhgrfun | ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) ) |
3 | eqid | ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) | |
4 | 1 3 | edg0iedg0 | ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |
5 | 2 4 | syl | ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |