Theorem dfacycgr1

Description: An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023)

	Ref	Expression
Assertion	dfacycgr1	|- AcyclicGraph = { g | A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) }

Proof

Step	Hyp	Ref	Expression
1		df-acycgr	|- AcyclicGraph = { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) }
2		2exanali	|- ( -. E. f E. p ( f ( Cycles ` g ) p /\ -. f = (/) ) <-> A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) )
3		df-ne	|- ( f =/= (/) <-> -. f = (/) )
4	3	anbi2i	|- ( ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> ( f ( Cycles ` g ) p /\ -. f = (/) ) )
5	4	2exbii	|- ( E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> E. f E. p ( f ( Cycles ` g ) p /\ -. f = (/) ) )
6	2 5	xchnxbir	|- ( -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) <-> A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) )
7	6	abbii	|- { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) } = { g | A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) }
8	1 7	eqtri	|- AcyclicGraph = { g | A. f A. p ( f ( Cycles ` g ) p -> f = (/) ) }