Metamath Proof Explorer

Theorem lfuhgr2

Description: A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 lfuhgr.1 ⊢V=Vtx⁡G
2 lfuhgr.2 ⊢I=iEdg⁡G
3 1 2 lfuhgr ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔∀x∈Edg⁡G2≤x
4 uhgredgn0 ⊢G∈UHGraph∧x∈Edg⁡G→x∈𝒫Vtx⁡G∖∅
5 eldifsni ⊢x∈𝒫Vtx⁡G∖∅→x≠∅
6 4 5 syl ⊢G∈UHGraph∧x∈Edg⁡G→x≠∅
7 hashneq0 ⊢x∈V→0<x↔x≠∅
8 7 elv ⊢0<x↔x≠∅
9 6 8 sylibr ⊢G∈UHGraph∧x∈Edg⁡G→0<x
10 9 gt0ne0d ⊢G∈UHGraph∧x∈Edg⁡G→x≠0
11 hashxnn0 ⊢x∈V→x∈ℕ0*
12 11 elv ⊢x∈ℕ0*
13 xnn0n0n1ge2b ⊢x∈ℕ0*→x≠0∧x≠1↔2≤x
14 12 13 ax-mp ⊢x≠0∧x≠1↔2≤x
15 14 biimpi ⊢x≠0∧x≠1→2≤x
16 10 15 stoic3 ⊢G∈UHGraph∧x∈Edg⁡G∧x≠1→2≤x
17 16 3exp ⊢G∈UHGraph→x∈Edg⁡G→x≠1→2≤x
18 17 a2d ⊢G∈UHGraph→x∈Edg⁡G→x≠1→x∈Edg⁡G→2≤x
19 18 ralimdv2 ⊢G∈UHGraph→∀x∈Edg⁡Gx≠1→∀x∈Edg⁡G2≤x
20 1xr ⊢1∈ℝ*
21 hashxrcl ⊢x∈V→x∈ℝ*
22 21 elv ⊢x∈ℝ*
23 1lt2 ⊢1<2
24 2re ⊢2∈ℝ
25 24 rexri ⊢2∈ℝ*
26 xrltletr ⊢1∈ℝ*∧2∈ℝ*∧x∈ℝ*→1<2∧2≤x→1<x
27 20 25 22 26 mp3an ⊢1<2∧2≤x→1<x
28 23 27 mpan ⊢2≤x→1<x
29 xrltne ⊢1∈ℝ*∧x∈ℝ*∧1<x→x≠1
30 20 22 28 29 mp3an12i ⊢2≤x→x≠1
31 30 ralimi ⊢∀x∈Edg⁡G2≤x→∀x∈Edg⁡Gx≠1
32 19 31 impbid1 ⊢G∈UHGraph→∀x∈Edg⁡Gx≠1↔∀x∈Edg⁡G2≤x
33 3 32 bitr4d ⊢G∈UHGraph→I:dom⁡I⟶x∈𝒫V|2≤x↔∀x∈Edg⁡Gx≠1