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 rgenw 𝑥𝑋 ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 )
6 ss2rab ( { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ↔ ∀ 𝑥𝑋 ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 ) )
7 5 6 mpbir { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
8 wwlkssswwlksn ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ ( WWalks ‘ 𝐺 )
9 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 wwlkssswrd ( WWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )
11 8 10 sstri ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )
12 1 11 eqsstri 𝑋 ⊆ Word ( Vtx ‘ 𝐺 )
13 rabss2 ( 𝑋 ⊆ Word ( Vtx ‘ 𝐺 ) → { 𝑥𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } )
14 12 13 ax-mp { 𝑥𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
15 7 14 sstri { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
16 15 rgenw 𝑦𝑌 { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
17 disjwrdpfx Disj 𝑦𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 }
18 disjss2 ( ∀ 𝑦𝑌 { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → ( Disj 𝑦𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → Disj 𝑦𝑌 { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) )
19 16 17 18 mp2 Disj 𝑦𝑌 { 𝑥𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) }