Metamath Proof Explorer

Theorem lfuhgr3

Description: A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses lfuhgr3.1 ⊢V=Vtx⁡G
lfuhgr3.2 ⊢I=iEdg⁡G
Assertion lfuhgr3 ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔¬∃aa∈Edg⁡G

Proof

Step Hyp Ref Expression
1 lfuhgr3.1 ⊢V=Vtx⁡G
2 lfuhgr3.2 ⊢I=iEdg⁡G
3 1 2 lfuhgr2 ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔∀x∈Edg⁡Gx≠1
4 df-ne ⊢x≠1↔¬x=1
5 4 ralbii ⊢∀x∈Edg⁡Gx≠1↔∀x∈Edg⁡G¬x=1
6 ralnex ⊢∀x∈Edg⁡G¬x=1↔¬∃x∈Edg⁡Gx=1
7 df-rex ⊢∃x∈Edg⁡Gx=1↔∃xx∈Edg⁡G∧x=1
8 7 notbii ⊢¬∃x∈Edg⁡Gx=1↔¬∃xx∈Edg⁡G∧x=1
9 5 6 8 3bitri ⊢∀x∈Edg⁡Gx≠1↔¬∃xx∈Edg⁡G∧x=1
10 hashen1 ⊢x∈V→x=1↔x≈1𝑜
11 10 elv ⊢x=1↔x≈1𝑜
12 en1 ⊢x≈1𝑜↔∃ax=a
13 11 12 bitri ⊢x=1↔∃ax=a
14 13 anbi2i ⊢x∈Edg⁡G∧x=1↔x∈Edg⁡G∧∃ax=a
15 14 exbii ⊢∃xx∈Edg⁡G∧x=1↔∃xx∈Edg⁡G∧∃ax=a
16 15 notbii ⊢¬∃xx∈Edg⁡G∧x=1↔¬∃xx∈Edg⁡G∧∃ax=a
17 19.3v ⊢∀ax∈Edg⁡G↔x∈Edg⁡G
18 19.29 ⊢∀ax∈Edg⁡G∧∃ax=a→∃ax∈Edg⁡G∧x=a
19 17 18 sylanbr ⊢x∈Edg⁡G∧∃ax=a→∃ax∈Edg⁡G∧x=a
20 eleq1 ⊢x=a→x∈Edg⁡G↔a∈Edg⁡G
21 20 biimpac ⊢x∈Edg⁡G∧x=a→a∈Edg⁡G
22 21 eximi ⊢∃ax∈Edg⁡G∧x=a→∃aa∈Edg⁡G
23 19 22 syl ⊢x∈Edg⁡G∧∃ax=a→∃aa∈Edg⁡G
24 23 exlimiv ⊢∃xx∈Edg⁡G∧∃ax=a→∃aa∈Edg⁡G
25 dfclel ⊢a∈Edg⁡G↔∃xx=a∧x∈Edg⁡G
26 pm3.22 ⊢x=a∧x∈Edg⁡G→x∈Edg⁡G∧x=a
27 26 eximi ⊢∃xx=a∧x∈Edg⁡G→∃xx∈Edg⁡G∧x=a
28 25 27 sylbi ⊢a∈Edg⁡G→∃xx∈Edg⁡G∧x=a
29 28 eximi ⊢∃aa∈Edg⁡G→∃a∃xx∈Edg⁡G∧x=a
30 excomim ⊢∃a∃xx∈Edg⁡G∧x=a→∃x∃ax∈Edg⁡G∧x=a
31 19.40 ⊢∃ax∈Edg⁡G∧x=a→∃ax∈Edg⁡G∧∃ax=a
32 ax5e ⊢∃ax∈Edg⁡G→x∈Edg⁡G
33 32 anim1i ⊢∃ax∈Edg⁡G∧∃ax=a→x∈Edg⁡G∧∃ax=a
34 31 33 syl ⊢∃ax∈Edg⁡G∧x=a→x∈Edg⁡G∧∃ax=a
35 34 eximi ⊢∃x∃ax∈Edg⁡G∧x=a→∃xx∈Edg⁡G∧∃ax=a
36 29 30 35 3syl ⊢∃aa∈Edg⁡G→∃xx∈Edg⁡G∧∃ax=a
37 24 36 impbii ⊢∃xx∈Edg⁡G∧∃ax=a↔∃aa∈Edg⁡G
38 37 notbii ⊢¬∃xx∈Edg⁡G∧∃ax=a↔¬∃aa∈Edg⁡G
39 9 16 38 3bitri ⊢∀x∈Edg⁡Gx≠1↔¬∃aa∈Edg⁡G
40 3 39 bitrdi ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔¬∃aa∈Edg⁡G