Theorem clwwlknondisj

Description: The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

	Ref	Expression
Assertion	clwwlknondisj	⊢ Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon	⊢ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑥 }
2		clwwlknon	⊢ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑦 }
3	1 2	ineq12i	⊢ ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∩ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑥 } ∩ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑦 } )
4		inrab	⊢ ( { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑥 } ∩ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑦 } ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) }
5		eqtr2	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) → 𝑥 = 𝑦 )
6	5	con3i	⊢ ( ¬ 𝑥 = 𝑦 → ¬ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) )
7	6	ralrimivw	⊢ ( ¬ 𝑥 = 𝑦 → ∀ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ¬ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) )
8		rabeq0	⊢ ( { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ¬ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) )
9	7 8	sylibr	⊢ ( ¬ 𝑥 = 𝑦 → { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑥 ∧ ( 𝑤 ‘ 0 ) = 𝑦 ) } = ∅ )
10	4 9	eqtrid	⊢ ( ¬ 𝑥 = 𝑦 → ( { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑥 } ∩ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑦 } ) = ∅ )
11	3 10	eqtrid	⊢ ( ¬ 𝑥 = 𝑦 → ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∩ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ∅ )
12	11	orri	⊢ ( 𝑥 = 𝑦 ∨ ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∩ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ∅ )
13	12	rgen2w	⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 = 𝑦 ∨ ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∩ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ∅ )
14		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
15	14	disjor	⊢ ( Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 = 𝑦 ∨ ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∩ ( 𝑦 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ∅ ) )
16	13 15	mpbir	⊢ Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 )