Metamath Proof Explorer

Theorem acycgrislfgr

Description: An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses acycgrislfgr.1 ⊢ V = Vtx ⁡ G
acycgrislfgr.2 ⊢ I = iEdg ⁡ G
Assertion acycgrislfgr ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x

Proof

Step Hyp Ref Expression
1 acycgrislfgr.1 ⊢ V = Vtx ⁡ G
2 acycgrislfgr.2 ⊢ I = iEdg ⁡ G
3 isacycgr ⊢ G ∈ UHGraph → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
4 3 biimpac ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
5 loop1cycl ⊢ G ∈ UHGraph → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1 ∧ p ⁡ 0 = a ↔ a ∈ Edg ⁡ G
6 3simpa ⊢ f Cycles ⁡ G p ∧ f = 1 ∧ p ⁡ 0 = a → f Cycles ⁡ G p ∧ f = 1
7 6 2eximi ⊢ ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1 ∧ p ⁡ 0 = a → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1
8 5 7 biimtrrdi ⊢ G ∈ UHGraph → a ∈ Edg ⁡ G → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1
9 8 exlimdv ⊢ G ∈ UHGraph → ∃ a a ∈ Edg ⁡ G → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1
10 vex ⊢ f ∈ V
11 hash1n0 ⊢ f ∈ V ∧ f = 1 → f ≠ ∅
12 10 11 mpan ⊢ f = 1 → f ≠ ∅
13 12 anim2i ⊢ f Cycles ⁡ G p ∧ f = 1 → f Cycles ⁡ G p ∧ f ≠ ∅
14 13 2eximi ⊢ ∃ f ∃ p f Cycles ⁡ G p ∧ f = 1 → ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
15 9 14 syl6 ⊢ G ∈ UHGraph → ∃ a a ∈ Edg ⁡ G → ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
16 15 con3d ⊢ G ∈ UHGraph → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅ → ¬ ∃ a a ∈ Edg ⁡ G
17 16 adantl ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅ → ¬ ∃ a a ∈ Edg ⁡ G
18 4 17 mpd ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → ¬ ∃ a a ∈ Edg ⁡ G
19 1 2 lfuhgr3 ⊢ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ ¬ ∃ a a ∈ Edg ⁡ G
20 19 adantl ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ ¬ ∃ a a ∈ Edg ⁡ G
21 18 20 mpbird ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x