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	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	1hegrlfgr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	1hegrlfgr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	1hegrlfgr.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	1hegrlfgr.x	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
	1hegrlfgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
	1hegrlfgr.e	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
Assertion	1hegrlfgr	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		1hegrlfgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
2		1hegrlfgr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		1hegrlfgr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		1hegrlfgr.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5		1hegrlfgr.x	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
6		1hegrlfgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
7		1hegrlfgr.e	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
8		f1osng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝒫 𝑉 ) → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐸 } )
9	1 5 8	syl2anc	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐸 } )
10		f1of	⊢ ( { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐸 } → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝐸 } )
11	9 10	syl	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝐸 } )
12		prid1g	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 , 𝐶 } )
13	2 12	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
14	7 13	sseldd	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
15		prid2g	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ { 𝐵 , 𝐶 } )
16	3 15	syl	⊢ ( 𝜑 → 𝐶 ∈ { 𝐵 , 𝐶 } )
17	7 16	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝐸 )
18	5 14 17 4	nehash2	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
19		fveq2	⊢ ( 𝑥 = 𝐸 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐸 ) )
20	19	breq2d	⊢ ( 𝑥 = 𝐸 → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ ( ♯ ‘ 𝐸 ) ) )
21	20	elrab	⊢ ( 𝐸 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ ( 𝐸 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝐸 ) ) )
22	5 18 21	sylanbrc	⊢ ( 𝜑 → 𝐸 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
23	22	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
24	11 23	fssd	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
25	6	feq1d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
26	24 25	mpbird	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )