Theorem numclwwlk3lem2lem

Description: Lemma for numclwwlk3lem2 : The set of closed vertices of a fixed length N on a fixed vertex V is the union of the set of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by AV, 1-May-2022)

	Ref	Expression
Hypotheses	numclwwlk3lem2.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
	numclwwlk3lem2.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion	numclwwlk3lem2lem	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3lem2.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2		numclwwlk3lem2.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
3	2	numclwwlkovh0	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } )
4	1	2clwwlk	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } )
5	3 4	uneq12d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) = ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∪ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) )
6		unrab	⊢ ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∪ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
7		exmidne	⊢ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 )
8		orcom	⊢ ( ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) )
9	7 8	mpbir	⊢ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
10	9	a1i	⊢ ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
11	10	rabeqc	⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ∨ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )
12	6 11	eqtri	⊢ ( { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∪ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )
13	5 12	eqtr2di	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( ( 𝑋 𝐻 𝑁 ) ∪ ( 𝑋 𝐶 𝑁 ) ) )