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 bitrdi G UHGraph I : dom I x 𝒫 V | 2 x ¬ a a Edg G