Metamath Proof Explorer

Theorem acycgrcycl

Description: Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Assertion acycgrcycl 
|- ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> F = (/) )

Proof

Step Hyp Ref Expression
1 cycliswlk 
 |-  ( F ( Cycles ` G ) P -> F ( Walks ` G ) P )
2 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
3 1 2 syl 
 |-  ( F ( Cycles ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
4 3 simp2d 
 |-  ( F ( Cycles ` G ) P -> F e. _V )
5 4 adantl 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> F e. _V )
6 3 simp3d 
 |-  ( F ( Cycles ` G ) P -> P e. _V )
7 6 adantl 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> P e. _V )
8 breq1 
 |-  ( f = F -> ( f ( Cycles ` G ) p <-> F ( Cycles ` G ) p ) )
9 eqeq1 
 |-  ( f = F -> ( f = (/) <-> F = (/) ) )
10 8 9 imbi12d 
 |-  ( f = F -> ( ( f ( Cycles ` G ) p -> f = (/) ) <-> ( F ( Cycles ` G ) p -> F = (/) ) ) )
11 breq2 
 |-  ( p = P -> ( F ( Cycles ` G ) p <-> F ( Cycles ` G ) P ) )
12 11 imbi1d 
 |-  ( p = P -> ( ( F ( Cycles ` G ) p -> F = (/) ) <-> ( F ( Cycles ` G ) P -> F = (/) ) ) )
13 10 12 sylan9bb 
 |-  ( ( f = F /\ p = P ) -> ( ( f ( Cycles ` G ) p -> f = (/) ) <-> ( F ( Cycles ` G ) P -> F = (/) ) ) )
14 isacycgr1 
 |-  ( G e. AcyclicGraph -> ( G e. AcyclicGraph <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )
15 14 ibi 
 |-  ( G e. AcyclicGraph -> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) )
16 15 19.21bbi 
 |-  ( G e. AcyclicGraph -> ( f ( Cycles ` G ) p -> f = (/) ) )
17 16 adantr 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> ( f ( Cycles ` G ) p -> f = (/) ) )
18 5 7 13 17 vtocl2d 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> ( F ( Cycles ` G ) P -> F = (/) ) )
19 18 ex 
 |-  ( G e. AcyclicGraph -> ( F ( Cycles ` G ) P -> ( F ( Cycles ` G ) P -> F = (/) ) ) )
20 19 pm2.43d 
 |-  ( G e. AcyclicGraph -> ( F ( Cycles ` G ) P -> F = (/) ) )
21 20 imp 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> F = (/) )