MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjxwwlksn Structured version   Visualization version   GIF version

Theorem disjxwwlksn 27690
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
StepHypRef Expression
1 simp1 1133 . . . . 5 (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦)
21a1i 11 . . . 4 (𝑥 ∈ Word 𝑉 → (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦))
32ss2rabi 4004 . . 3 {𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
43rgenw 3118 . 2 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
5 disjwrdpfx 14053 . 2 Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
6 disjss2 4998 . 2 (∀𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} → (Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} → Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}))
74, 5, 6mp2 9 1 Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2111  wral 3106  {crab 3110  wss 3881  {cpr 4527  Disj wdisj 4995  cfv 6324  (class class class)co 7135  0cc0 10526  Word cword 13857  lastSclsw 13905   prefix cpfx 14023  Vtxcvtx 26789  Edgcedg 26840   WWalksN cwwlksn 27612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-in 3888  df-ss 3898  df-disj 4996
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator