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 ⊢ V = Vtx ⁡ G
lfuhgr.2 ⊢ I = iEdg ⁡ G
Assertion lfuhgr ⊢ G ∈ UHGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ ∀ x ∈ Edg ⁡ G 2 ≤ x

Proof

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