Theorem clwwlkneq0

Description: Sufficient conditions for ClWWalksN to be empty. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 24-Feb-2022)

	Ref	Expression
Assertion	clwwlkneq0	|- ( ( G e/ _V \/ N e/ NN ) -> ( N ClWWalksN G ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-nel	|- ( G e/ _V <-> -. G e. _V )
2		ianor	|- ( -. ( N e. NN0 /\ N =/= 0 ) <-> ( -. N e. NN0 \/ -. N =/= 0 ) )
3	1 2	orbi12i	|- ( ( G e/ _V \/ -. ( N e. NN0 /\ N =/= 0 ) ) <-> ( -. G e. _V \/ ( -. N e. NN0 \/ -. N =/= 0 ) ) )
4		df-nel	|- ( N e/ NN <-> -. N e. NN )
5		elnnne0	|- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
6	4 5	xchbinx	|- ( N e/ NN <-> -. ( N e. NN0 /\ N =/= 0 ) )
7	6	orbi2i	|- ( ( G e/ _V \/ N e/ NN ) <-> ( G e/ _V \/ -. ( N e. NN0 /\ N =/= 0 ) ) )
8		orass	|- ( ( ( -. G e. _V \/ -. N e. NN0 ) \/ -. N =/= 0 ) <-> ( -. G e. _V \/ ( -. N e. NN0 \/ -. N =/= 0 ) ) )
9	3 7 8	3bitr4i	|- ( ( G e/ _V \/ N e/ NN ) <-> ( ( -. G e. _V \/ -. N e. NN0 ) \/ -. N =/= 0 ) )
10		ianor	|- ( -. ( N e. NN0 /\ G e. _V ) <-> ( -. N e. NN0 \/ -. G e. _V ) )
11		orcom	|- ( ( -. N e. NN0 \/ -. G e. _V ) <-> ( -. G e. _V \/ -. N e. NN0 ) )
12	10 11	bitri	|- ( -. ( N e. NN0 /\ G e. _V ) <-> ( -. G e. _V \/ -. N e. NN0 ) )
13		df-clwwlkn	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. ( ClWWalks ` g ) | ( # ` w ) = n } )
14	13	mpondm0	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( N ClWWalksN G ) = (/) )
15	12 14	sylbir	|- ( ( -. G e. _V \/ -. N e. NN0 ) -> ( N ClWWalksN G ) = (/) )
16		nne	|- ( -. N =/= 0 <-> N = 0 )
17		oveq1	|- ( N = 0 -> ( N ClWWalksN G ) = ( 0 ClWWalksN G ) )
18		clwwlkn0	|- ( 0 ClWWalksN G ) = (/)
19	17 18	eqtrdi	|- ( N = 0 -> ( N ClWWalksN G ) = (/) )
20	16 19	sylbi	|- ( -. N =/= 0 -> ( N ClWWalksN G ) = (/) )
21	15 20	jaoi	|- ( ( ( -. G e. _V \/ -. N e. NN0 ) \/ -. N =/= 0 ) -> ( N ClWWalksN G ) = (/) )
22	9 21	sylbi	|- ( ( G e/ _V \/ N e/ NN ) -> ( N ClWWalksN G ) = (/) )