Metamath Proof Explorer

Theorem acycgrsubgr

Description: The subgraph of an acyclic graph is also acyclic. (Contributed by BTernaryTau, 23-Oct-2023)

Ref Expression
Assertion acycgrsubgr 
|- ( ( G e. AcyclicGraph /\ S SubGraph G ) -> S e. AcyclicGraph )

Proof

Step Hyp Ref Expression
1 subgrcycl 
 |-  ( S SubGraph G -> ( f ( Cycles ` S ) p -> f ( Cycles ` G ) p ) )
2 1 anim1d 
 |-  ( S SubGraph G -> ( ( f ( Cycles ` S ) p /\ f =/= (/) ) -> ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
3 2 2eximdv 
 |-  ( S SubGraph G -> ( E. f E. p ( f ( Cycles ` S ) p /\ f =/= (/) ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
4 3 con3d 
 |-  ( S SubGraph G -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. E. f E. p ( f ( Cycles ` S ) p /\ f =/= (/) ) ) )
5 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
6 isacycgr 
 |-  ( G e. _V -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
7 5 6 simpl2im 
 |-  ( S SubGraph G -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
8 5 simpld 
 |-  ( S SubGraph G -> S e. _V )
9 isacycgr 
 |-  ( S e. _V -> ( S e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` S ) p /\ f =/= (/) ) ) )
10 8 9 syl 
 |-  ( S SubGraph G -> ( S e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` S ) p /\ f =/= (/) ) ) )
11 4 7 10 3imtr4d 
 |-  ( S SubGraph G -> ( G e. AcyclicGraph -> S e. AcyclicGraph ) )
12 11 impcom 
 |-  ( ( G e. AcyclicGraph /\ S SubGraph G ) -> S e. AcyclicGraph )