This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑥 ) } ∈ 𝐸 ) }