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

Metamath Proof Explorer

Theorem disjxwwlkn

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, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
Assertion disjxwwlkn Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) }

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
2 wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
4 simp1 ⊢ ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 )
5 4 a1i ⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 ) )
6 5 ss2rabi ⊢ { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
7 wwlkssswwlksn ⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ ( WWalks ‘ 𝐺 )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 8 wwlkssswrd ⊢ ( WWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )
10 7 9 sstri ⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )
11 1 10 eqsstri ⊢ 𝑋 ⊆ Word ( Vtx ‘ 𝐺 )
12 rabss2 ⊢ ( 𝑋 ⊆ Word ( Vtx ‘ 𝐺 ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } )
13 11 12 ax-mp ⊢ { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
14 6 13 sstri ⊢ { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
15 14 rgenw ⊢ ∀ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
16 disjwrdpfx ⊢ Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
17 disjss2 ⊢ ( ∀ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → ( Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) )
18 15 16 17 mp2 ⊢ Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) }