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 G 2 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 syl5bb 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 G 2 x
21 20 baib Edg G 𝒫 V Edg G x 𝒫 V | 2 x x Edg G 2 x
22 19 21 syl G UHGraph Edg G x 𝒫 V | 2 x x Edg G 2 x
23 15 22 bitr3d G UHGraph I : dom I x 𝒫 V | 2 x x Edg G 2 x