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