Theorem lfgrnloop

Description: A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	lfuhgrnloopv.i	|- I = ( iEdg ` G )
	lfuhgrnloopv.a	|- A = dom I
	lfuhgrnloopv.e	|- E = { x e. ~P V | 2 <_ ( # ` x ) }
Assertion	lfgrnloop	|- ( I : A --> E -> { x e. A | ( I ` x ) = { U } } = (/) )

Proof

Step	Hyp	Ref	Expression
1		lfuhgrnloopv.i	|- I = ( iEdg ` G )
2		lfuhgrnloopv.a	|- A = dom I
3		lfuhgrnloopv.e	|- E = { x e. ~P V | 2 <_ ( # ` x ) }
4		nfcv	|- F/_ x I
5		nfcv	|- F/_ x A
6		nfrab1	|- F/_ x { x e. ~P V | 2 <_ ( # ` x ) }
7	3 6	nfcxfr	|- F/_ x E
8	4 5 7	nff	|- F/ x I : A --> E
9		hashsn01	|- ( ( # ` { U } ) = 0 \/ ( # ` { U } ) = 1 )
10		2pos	|- 0 < 2
11		0re	|- 0 e. RR
12		2re	|- 2 e. RR
13	11 12	ltnlei	|- ( 0 < 2 <-> -. 2 <_ 0 )
14	10 13	mpbi	|- -. 2 <_ 0
15		breq2	|- ( ( # ` { U } ) = 0 -> ( 2 <_ ( # ` { U } ) <-> 2 <_ 0 ) )
16	14 15	mtbiri	|- ( ( # ` { U } ) = 0 -> -. 2 <_ ( # ` { U } ) )
17		1lt2	|- 1 < 2
18		1re	|- 1 e. RR
19	18 12	ltnlei	|- ( 1 < 2 <-> -. 2 <_ 1 )
20	17 19	mpbi	|- -. 2 <_ 1
21		breq2	|- ( ( # ` { U } ) = 1 -> ( 2 <_ ( # ` { U } ) <-> 2 <_ 1 ) )
22	20 21	mtbiri	|- ( ( # ` { U } ) = 1 -> -. 2 <_ ( # ` { U } ) )
23	16 22	jaoi	|- ( ( ( # ` { U } ) = 0 \/ ( # ` { U } ) = 1 ) -> -. 2 <_ ( # ` { U } ) )
24	9 23	ax-mp	|- -. 2 <_ ( # ` { U } )
25		fveq2	|- ( ( I ` x ) = { U } -> ( # ` ( I ` x ) ) = ( # ` { U } ) )
26	25	breq2d	|- ( ( I ` x ) = { U } -> ( 2 <_ ( # ` ( I ` x ) ) <-> 2 <_ ( # ` { U } ) ) )
27	24 26	mtbiri	|- ( ( I ` x ) = { U } -> -. 2 <_ ( # ` ( I ` x ) ) )
28	1 2 3	lfgredgge2	|- ( ( I : A --> E /\ x e. A ) -> 2 <_ ( # ` ( I ` x ) ) )
29	27 28	nsyl3	|- ( ( I : A --> E /\ x e. A ) -> -. ( I ` x ) = { U } )
30	29	ex	|- ( I : A --> E -> ( x e. A -> -. ( I ` x ) = { U } ) )
31	8 30	ralrimi	|- ( I : A --> E -> A. x e. A -. ( I ` x ) = { U } )
32		rabeq0	|- ( { x e. A | ( I ` x ) = { U } } = (/) <-> A. x e. A -. ( I ` x ) = { U } )
33	31 32	sylibr	|- ( I : A --> E -> { x e. A | ( I ` x ) = { U } } = (/) )