Theorem crctcshlem1

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)

	Ref	Expression
Hypotheses	crctcsh.v	|- V = ( Vtx ` G )
	crctcsh.i	|- I = ( iEdg ` G )
	crctcsh.d	|- ( ph -> F ( Circuits ` G ) P )
	crctcsh.n	|- N = ( # ` F )
Assertion	crctcshlem1	|- ( ph -> N e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	|- V = ( Vtx ` G )
2		crctcsh.i	|- I = ( iEdg ` G )
3		crctcsh.d	|- ( ph -> F ( Circuits ` G ) P )
4		crctcsh.n	|- N = ( # ` F )
5		crctiswlk	|- ( F ( Circuits ` G ) P -> F ( Walks ` G ) P )
6		wlkcl	|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
7	4 6	eqeltrid	|- ( F ( Walks ` G ) P -> N e. NN0 )
8	3 5 7	3syl	|- ( ph -> N e. NN0 )