Metamath Proof Explorer

Theorem lfuhgr

Description: A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses lfuhgr.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
lfuhgr.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion lfuhgr ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) 2 ≤ ( ♯ ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 lfuhgr.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 lfuhgr.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 2 rneqi ⊢ ran 𝐼 = ran ( iEdg ‘ 𝐺 )
5 3 4 eqtr4i ⊢ ( Edg ‘ 𝐺 ) = ran 𝐼
6 5 sseq1i ⊢ ( ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
7 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
8 fdmrn ⊢ ( Fun 𝐼 ↔ 𝐼 : dom 𝐼 ⟶ ran 𝐼 )
9 fss ⊢ ( ( 𝐼 : dom 𝐼 ⟶ ran 𝐼 ∧ ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
10 9 ex ⊢ ( 𝐼 : dom 𝐼 ⟶ ran 𝐼 → ( ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
11 8 10 sylbi ⊢ ( Fun 𝐼 → ( ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
12 7 11 syl ⊢ ( 𝐺 ∈ UHGraph → ( ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
13 frn ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
14 12 13 impbid1 ⊢ ( 𝐺 ∈ UHGraph → ( ran 𝐼 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
15 6 14 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
16 uhgredgss ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) ⊆ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
17 16 difss2d ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) ⊆ 𝒫 ( Vtx ‘ 𝐺 ) )
18 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐺 )
19 17 18 sseqtrrdi ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) ⊆ 𝒫 𝑉 )
20 ssrab ⊢ ( ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ( ( Edg ‘ 𝐺 ) ⊆ 𝒫 𝑉 ∧ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) 2 ≤ ( ♯ ‘ 𝑥 ) ) )
21 20 baib ⊢ ( ( Edg ‘ 𝐺 ) ⊆ 𝒫 𝑉 → ( ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) 2 ≤ ( ♯ ‘ 𝑥 ) ) )
22 19 21 syl ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) 2 ≤ ( ♯ ‘ 𝑥 ) ) )
23 15 22 bitr3d ⊢ ( 𝐺 ∈ UHGraph → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) 2 ≤ ( ♯ ‘ 𝑥 ) ) )