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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
lfuhgr.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion lfuhgr2 ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) ≠ 1 ) )

Proof

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