Metamath Proof Explorer


Theorem lfgrnloop

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

Ref Expression
Hypotheses lfuhgrnloopv.i I=iEdgG
lfuhgrnloopv.a A=domI
lfuhgrnloopv.e E=x𝒫V|2x
Assertion lfgrnloop I:AExA|Ix=U=

Proof

Step Hyp Ref Expression
1 lfuhgrnloopv.i I=iEdgG
2 lfuhgrnloopv.a A=domI
3 lfuhgrnloopv.e E=x𝒫V|2x
4 nfcv _xI
5 nfcv _xA
6 nfrab1 _xx𝒫V|2x
7 3 6 nfcxfr _xE
8 4 5 7 nff xI:AE
9 hashsn01 U=0U=1
10 2pos 0<2
11 0re 0
12 2re 2
13 11 12 ltnlei 0<2¬20
14 10 13 mpbi ¬20
15 breq2 U=02U20
16 14 15 mtbiri U=0¬2U
17 1lt2 1<2
18 1re 1
19 18 12 ltnlei 1<2¬21
20 17 19 mpbi ¬21
21 breq2 U=12U21
22 20 21 mtbiri U=1¬2U
23 16 22 jaoi U=0U=1¬2U
24 9 23 ax-mp ¬2U
25 fveq2 Ix=UIx=U
26 25 breq2d Ix=U2Ix2U
27 24 26 mtbiri Ix=U¬2Ix
28 1 2 3 lfgredgge2 I:AExA2Ix
29 27 28 nsyl3 I:AExA¬Ix=U
30 29 ex I:AExA¬Ix=U
31 8 30 ralrimi I:AExA¬Ix=U
32 rabeq0 xA|Ix=U=xA¬Ix=U
33 31 32 sylibr I:AExA|Ix=U=