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 ⁡ G x ≠ 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 ⁡ G 2 ≤ 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 ⁡ G x ≠ 1 → ∀ x ∈ Edg ⁡ G 2 ≤ 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 ⁡ G 2 ≤ x → ∀ x ∈ Edg ⁡ G x ≠ 1
32 19 31 impbid1 ⊢ G ∈ UHGraph → ∀ x ∈ Edg ⁡ G x ≠ 1 ↔ ∀ x ∈ Edg ⁡ G 2 ≤ x
33 3 32 bitr4d ⊢ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ ∀ x ∈ Edg ⁡ G x ≠ 1