Theorem disjxwwlksn 29934

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.)

Hypotheses

Ref	Expression
wwlksnexthasheq.v	⊢ 𝑉 = (Vtx‘𝐺)
wwlksnexthasheq.e	⊢ 𝐸 = (Edg‘𝐺)

Assertion

Ref	Expression
disjxwwlksn	⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}

Distinct variable groups:   𝑦,𝑁   𝑥,𝑉   𝑥,𝑦

Allowed substitution hints:   𝑃(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝑁(𝑥)   𝑉(𝑦)

Proof of Theorem disjxwwlksn

Step	Hyp	Ref	Expression
1		simp1 1135	. . . . 5 ⊢ (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦)
2	1	a1i 11	. . . 4 ⊢ (𝑥 ∈ Word 𝑉 → (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦))
3	2	ss2rabi 4087	. . 3 ⊢ {𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
4	3	rgenw 3063	. 2 ⊢ ∀𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
5		disjwrdpfx 14735	. 2 ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
6		disjss2 5118	. 2 ⊢ (∀𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} → (Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} → Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}))
7	4, 5, 6	mp2 9	1 ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  ∀wral 3059  {crab 3433   ⊆ wss 3963  {cpr 4633  Disj wdisj 5115  ‘cfv 6563  (class class class)co 7431  0cc0 11153  Word cword 14549  lastSclsw 14597   prefix cpfx 14705  Vtxcvtx 29028  Edgcedg 29079   WWalksN cwwlksn 29856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rmo 3378  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-ss 3980  df-disj 5116

This theorem is referenced by: (None)