Theorem isacycgr1

Description: The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023)

	Ref	Expression
Assertion	isacycgr1	|- ( G e. W -> ( G e. AcyclicGraph <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( g = G -> ( Cycles ` g ) = ( Cycles ` G ) )
2	1	breqd	|- ( g = G -> ( f ( Cycles ` g ) p <-> f ( Cycles ` G ) p ) )
3	2	imbi1d	|- ( g = G -> ( ( f ( Cycles ` g ) p -> f = (/) ) <-> ( f ( Cycles ` G ) p -> f = (/) ) ) )
4	3	2albidv	|- ( g = G -> ( A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )
5		dfacycgr1	|- AcyclicGraph = { g | A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) }
6	4 5	elab2g	|- ( G e. W -> ( G e. AcyclicGraph <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )