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

Proof

Step Hyp Ref Expression
1 lfuhgr3.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 lfuhgr3.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 lfuhgr2 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) ≠ 1 ) )
4 df-ne ⊢ ( ( ♯ ‘ 𝑥 ) ≠ 1 ↔ ¬ ( ♯ ‘ 𝑥 ) = 1 )
5 4 ralbii ⊢ ( ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) ≠ 1 ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑥 ) = 1 )
6 ralnex ⊢ ( ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ¬ ( ♯ ‘ 𝑥 ) = 1 ↔ ¬ ∃ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 1 )
7 df-rex ⊢ ( ∃ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 1 ↔ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) )
8 7 notbii ⊢ ( ¬ ∃ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 1 ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) )
9 5 6 8 3bitri ⊢ ( ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) ≠ 1 ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) )
10 hashen1 ⊢ ( 𝑥 ∈ V → ( ( ♯ ‘ 𝑥 ) = 1 ↔ 𝑥 ≈ 1o ) )
11 10 elv ⊢ ( ( ♯ ‘ 𝑥 ) = 1 ↔ 𝑥 ≈ 1o )
12 en1 ⊢ ( 𝑥 ≈ 1o ↔ ∃ 𝑎 𝑥 = { 𝑎 } )
13 11 12 bitri ⊢ ( ( ♯ ‘ 𝑥 ) = 1 ↔ ∃ 𝑎 𝑥 = { 𝑎 } )
14 13 anbi2i ⊢ ( ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) ↔ ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
15 14 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
16 15 notbii ⊢ ( ¬ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
17 19.3v ⊢ ( ∀ 𝑎 𝑥 ∈ ( Edg ‘ 𝐺 ) ↔ 𝑥 ∈ ( Edg ‘ 𝐺 ) )
18 19.29 ⊢ ( ( ∀ 𝑎 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) → ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
19 17 18 sylanbr ⊢ ( ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) → ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
20 eleq1 ⊢ ( 𝑥 = { 𝑎 } → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
21 20 biimpac ⊢ ( ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
22 21 eximi ⊢ ( ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
23 19 22 syl ⊢ ( ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) → ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
24 23 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) → ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
25 dfclel ⊢ ( { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ( 𝑥 = { 𝑎 } ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ) )
26 pm3.22 ⊢ ( ( 𝑥 = { 𝑎 } ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
27 26 eximi ⊢ ( ∃ 𝑥 ( 𝑥 = { 𝑎 } ∧ 𝑥 ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
28 25 27 sylbi ⊢ ( { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
29 28 eximi ⊢ ( ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑎 ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
30 excomim ⊢ ( ∃ 𝑎 ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → ∃ 𝑥 ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) )
31 19.40 ⊢ ( ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → ( ∃ 𝑎 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
32 ax5e ⊢ ( ∃ 𝑎 𝑥 ∈ ( Edg ‘ 𝐺 ) → 𝑥 ∈ ( Edg ‘ 𝐺 ) )
33 32 anim1i ⊢ ( ( ∃ 𝑎 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
34 31 33 syl ⊢ ( ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
35 34 eximi ⊢ ( ∃ 𝑥 ∃ 𝑎 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑥 = { 𝑎 } ) → ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
36 29 30 35 3syl ⊢ ( ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) )
37 24 36 impbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) ↔ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
38 37 notbii ⊢ ( ¬ ∃ 𝑥 ( 𝑥 ∈ ( Edg ‘ 𝐺 ) ∧ ∃ 𝑎 𝑥 = { 𝑎 } ) ↔ ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
39 9 16 38 3bitri ⊢ ( ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) ≠ 1 ↔ ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
40 3 39 bitrdi ⊢ ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ¬ ∃ 𝑎 { 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )