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 ‘ 𝐺 ) = ∅ ) ) |