Theorem disjxwwlksn

Description: Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 27-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnexthasheq.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wwlksnexthasheq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	disjxwwlksn	⊢ Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) }

Proof

Step	Hyp	Ref	Expression
1		wwlksnexthasheq.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wwlksnexthasheq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		simp1	⊢ ( ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑁 ) = 𝑦 )
4	3	a1i	⊢ ( 𝑥 ∈ Word 𝑉 → ( ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑁 ) = 𝑦 ) )
5	4	ss2rabi	⊢ { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 }
6	5	rgenw	⊢ ∀ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 }
7		disjwrdpfx	⊢ Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 }
8		disjss2	⊢ ( ∀ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } → ( Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } → Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) )
9	6 7 8	mp2	⊢ Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) }