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