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