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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
acycgrislfgr.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion acycgrislfgr ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 acycgrislfgr.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 acycgrislfgr.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 isacycgr ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
4 3 biimpac ⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
5 loop1cycl ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) ↔ { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
6 3simpa ⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) )
7 6 2eximi ⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) )
8 5 7 syl6bir ⊢ ( 𝐺 ∈ UHGraph → ( { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) ) )
9 8 exlimdv ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) ) )
10 vex ⊢ 𝑓 ∈ V
11 hash1n0 ⊢ ( ( 𝑓 ∈ V ∧ ( ♯ ‘ 𝑓 ) = 1 ) → 𝑓 ≠ ∅ )
12 10 11 mpan ⊢ ( ( ♯ ‘ 𝑓 ) = 1 → 𝑓 ≠ ∅ )
13 12 anim2i ⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
14 13 2eximi ⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 1 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
15 9 14 syl6 ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
16 15 con3d ⊢ ( 𝐺 ∈ UHGraph → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
17 16 adantl ⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
18 4 17 mpd ⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
19 1 2 lfuhgr3 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
20 19 adantl ⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
21 18 20 mpbird ⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )