Metamath Proof Explorer

Theorem 1hegrlfgr

Description: A graph G with one hyperedge joining at least two vertices is a loop-free graph. (Contributed by AV, 23-Feb-2021)

Ref Expression
Hypotheses 1hegrlfgr.a ⊢ φ → A ∈ X
1hegrlfgr.b ⊢ φ → B ∈ V
1hegrlfgr.c ⊢ φ → C ∈ V
1hegrlfgr.n ⊢ φ → B ≠ C
1hegrlfgr.x ⊢ φ → E ∈ 𝒫 V
1hegrlfgr.i ⊢ φ → iEdg ⁡ G = A E
1hegrlfgr.e ⊢ φ → B C ⊆ E
Assertion 1hegrlfgr ⊢ φ → iEdg ⁡ G : A ⟶ x ∈ 𝒫 V | 2 ≤ x

Proof

Step Hyp Ref Expression
1 1hegrlfgr.a ⊢ φ → A ∈ X
2 1hegrlfgr.b ⊢ φ → B ∈ V
3 1hegrlfgr.c ⊢ φ → C ∈ V
4 1hegrlfgr.n ⊢ φ → B ≠ C
5 1hegrlfgr.x ⊢ φ → E ∈ 𝒫 V
6 1hegrlfgr.i ⊢ φ → iEdg ⁡ G = A E
7 1hegrlfgr.e ⊢ φ → B C ⊆ E
8 f1osng ⊢ A ∈ X ∧ E ∈ 𝒫 V → A E : A ⟶ 1-1 onto E
9 1 5 8 syl2anc ⊢ φ → A E : A ⟶ 1-1 onto E
10 f1of ⊢ A E : A ⟶ 1-1 onto E → A E : A ⟶ E
11 9 10 syl ⊢ φ → A E : A ⟶ E
12 prid1g ⊢ B ∈ V → B ∈ B C
13 2 12 syl ⊢ φ → B ∈ B C
14 7 13 sseldd ⊢ φ → B ∈ E
15 prid2g ⊢ C ∈ V → C ∈ B C
16 3 15 syl ⊢ φ → C ∈ B C
17 7 16 sseldd ⊢ φ → C ∈ E
18 5 14 17 4 nehash2 ⊢ φ → 2 ≤ E
19 fveq2 ⊢ x = E → x = E
20 19 breq2d ⊢ x = E → 2 ≤ x ↔ 2 ≤ E
21 20 elrab ⊢ E ∈ x ∈ 𝒫 V | 2 ≤ x ↔ E ∈ 𝒫 V ∧ 2 ≤ E
22 5 18 21 sylanbrc ⊢ φ → E ∈ x ∈ 𝒫 V | 2 ≤ x
23 22 snssd ⊢ φ → E ⊆ x ∈ 𝒫 V | 2 ≤ x
24 11 23 fssd ⊢ φ → A E : A ⟶ x ∈ 𝒫 V | 2 ≤ x
25 6 feq1d ⊢ φ → iEdg ⁡ G : A ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ A E : A ⟶ x ∈ 𝒫 V | 2 ≤ x
26 24 25 mpbird ⊢ φ → iEdg ⁡ G : A ⟶ x ∈ 𝒫 V | 2 ≤ x