Description: A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lfuhgrnloopv.i | |
|
lfuhgrnloopv.a | |
||
lfuhgrnloopv.e | |
||
Assertion | lfgrnloop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lfuhgrnloopv.i | |
|
2 | lfuhgrnloopv.a | |
|
3 | lfuhgrnloopv.e | |
|
4 | nfcv | |
|
5 | nfcv | |
|
6 | nfrab1 | |
|
7 | 3 6 | nfcxfr | |
8 | 4 5 7 | nff | |
9 | hashsn01 | |
|
10 | 2pos | |
|
11 | 0re | |
|
12 | 2re | |
|
13 | 11 12 | ltnlei | |
14 | 10 13 | mpbi | |
15 | breq2 | |
|
16 | 14 15 | mtbiri | |
17 | 1lt2 | |
|
18 | 1re | |
|
19 | 18 12 | ltnlei | |
20 | 17 19 | mpbi | |
21 | breq2 | |
|
22 | 20 21 | mtbiri | |
23 | 16 22 | jaoi | |
24 | 9 23 | ax-mp | |
25 | fveq2 | |
|
26 | 25 | breq2d | |
27 | 24 26 | mtbiri | |
28 | 1 2 3 | lfgredgge2 | |
29 | 27 28 | nsyl3 | |
30 | 29 | ex | |
31 | 8 30 | ralrimi | |
32 | rabeq0 | |
|
33 | 31 32 | sylibr | |