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	|- ( ph -> A e. X )
	1hegrlfgr.b	|- ( ph -> B e. V )
	1hegrlfgr.c	|- ( ph -> C e. V )
	1hegrlfgr.n	|- ( ph -> B =/= C )
	1hegrlfgr.x	|- ( ph -> E e. ~P V )
	1hegrlfgr.i	|- ( ph -> ( iEdg ` G ) = { <. A , E >. } )
	1hegrlfgr.e	|- ( ph -> { B , C } C_ E )
Assertion	1hegrlfgr	|- ( ph -> ( iEdg ` G ) : { A } --> { x e. ~P V | 2 <_ ( # ` x ) } )

Proof

Step	Hyp	Ref	Expression
1		1hegrlfgr.a	|- ( ph -> A e. X )
2		1hegrlfgr.b	|- ( ph -> B e. V )
3		1hegrlfgr.c	|- ( ph -> C e. V )
4		1hegrlfgr.n	|- ( ph -> B =/= C )
5		1hegrlfgr.x	|- ( ph -> E e. ~P V )
6		1hegrlfgr.i	|- ( ph -> ( iEdg ` G ) = { <. A , E >. } )
7		1hegrlfgr.e	|- ( ph -> { B , C } C_ E )
8		f1osng	|- ( ( A e. X /\ E e. ~P V ) -> { <. A , E >. } : { A } -1-1-onto-> { E } )
9	1 5 8	syl2anc	|- ( ph -> { <. A , E >. } : { A } -1-1-onto-> { E } )
10		f1of	|- ( { <. A , E >. } : { A } -1-1-onto-> { E } -> { <. A , E >. } : { A } --> { E } )
11	9 10	syl	|- ( ph -> { <. A , E >. } : { A } --> { E } )
12		prid1g	|- ( B e. V -> B e. { B , C } )
13	2 12	syl	|- ( ph -> B e. { B , C } )
14	7 13	sseldd	|- ( ph -> B e. E )
15		prid2g	|- ( C e. V -> C e. { B , C } )
16	3 15	syl	|- ( ph -> C e. { B , C } )
17	7 16	sseldd	|- ( ph -> C e. E )
18	5 14 17 4	nehash2	|- ( ph -> 2 <_ ( # ` E ) )
19		fveq2	|- ( x = E -> ( # ` x ) = ( # ` E ) )
20	19	breq2d	|- ( x = E -> ( 2 <_ ( # ` x ) <-> 2 <_ ( # ` E ) ) )
21	20	elrab	|- ( E e. { x e. ~P V | 2 <_ ( # ` x ) } <-> ( E e. ~P V /\ 2 <_ ( # ` E ) ) )
22	5 18 21	sylanbrc	|- ( ph -> E e. { x e. ~P V | 2 <_ ( # ` x ) } )
23	22	snssd	|- ( ph -> { E } C_ { x e. ~P V | 2 <_ ( # ` x ) } )
24	11 23	fssd	|- ( ph -> { <. A , E >. } : { A } --> { x e. ~P V | 2 <_ ( # ` x ) } )
25	6	feq1d	|- ( ph -> ( ( iEdg ` G ) : { A } --> { x e. ~P V | 2 <_ ( # ` x ) } <-> { <. A , E >. } : { A } --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
26	24 25	mpbird	|- ( ph -> ( iEdg ` G ) : { A } --> { x e. ~P V | 2 <_ ( # ` x ) } )