Theorem isacycgr

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

	Ref	Expression
Assertion	isacycgr	|- ( G e. W -> ( G e. AcyclicGraph <-> -. E. f E. 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	anbi1d	|- ( g = G -> ( ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
4	3	2exbidv	|- ( g = G -> ( E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
5	4	notbid	|- ( g = G -> ( -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
6		df-acycgr	|- AcyclicGraph = { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) }
7	5 6	elab2g	|- ( G e. W -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )