Metamath Proof Explorer

Theorem lfuhgr

Description: A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses lfuhgr.1 ⊢V=Vtx⁡G
lfuhgr.2 ⊢I=iEdg⁡G
Assertion lfuhgr ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔∀x∈Edg⁡G2≤x

Proof

Step Hyp Ref Expression
1 lfuhgr.1 ⊢V=Vtx⁡G
2 lfuhgr.2 ⊢I=iEdg⁡G
3 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
4 2 rneqi ⊢ran⁡I=ran⁡iEdg⁡G
5 3 4 eqtr4i ⊢Edg⁡G=ran⁡I
6 5 sseq1i ⊢Edg⁡G⊆x∈𝒫V|2≤x↔ran⁡I⊆x∈𝒫V|2≤x
7 2 uhgrfun ⊢G∈UHGraph→Fun⁡I
8 fdmrn ⊢Fun⁡I↔I:dom⁡I⟶ran⁡I
9 fss ⊢I:dom⁡I⟶ran⁡I∧ran⁡I⊆x∈𝒫V|2≤x→I:dom⁡I⟶x∈𝒫V|2≤x
10 9 ex ⊢I:dom⁡I⟶ran⁡I→ran⁡I⊆x∈𝒫V|2≤x→I:dom⁡I⟶x∈𝒫V|2≤x
11 8 10 sylbi ⊢Fun⁡I→ran⁡I⊆x∈𝒫V|2≤x→I:dom⁡I⟶x∈𝒫V|2≤x
12 7 11 syl ⊢G∈UHGraph→ran⁡I⊆x∈𝒫V|2≤x→I:dom⁡I⟶x∈𝒫V|2≤x
13 frn ⊢I:dom⁡I⟶x∈𝒫V|2≤x→ran⁡I⊆x∈𝒫V|2≤x
14 12 13 impbid1 ⊢G∈UHGraph→ran⁡I⊆x∈𝒫V|2≤x↔I:dom⁡I⟶x∈𝒫V|2≤x
15 6 14 bitrid ⊢G∈UHGraph→Edg⁡G⊆x∈𝒫V|2≤x↔I:dom⁡I⟶x∈𝒫V|2≤x
16 uhgredgss ⊢G∈UHGraph→Edg⁡G⊆𝒫Vtx⁡G∖∅
17 16 difss2d ⊢G∈UHGraph→Edg⁡G⊆𝒫Vtx⁡G
18 1 pweqi ⊢𝒫V=𝒫Vtx⁡G
19 17 18 sseqtrrdi ⊢G∈UHGraph→Edg⁡G⊆𝒫V
20 ssrab ⊢Edg⁡G⊆x∈𝒫V|2≤x↔Edg⁡G⊆𝒫V∧∀x∈Edg⁡G2≤x
21 20 baib ⊢Edg⁡G⊆𝒫V→Edg⁡G⊆x∈𝒫V|2≤x↔∀x∈Edg⁡G2≤x
22 19 21 syl ⊢G∈UHGraph→Edg⁡G⊆x∈𝒫V|2≤x↔∀x∈Edg⁡G2≤x
23 15 22 bitr3d ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔∀x∈Edg⁡G2≤x