Theorem disjxwwlksn 30162

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 1152	. . . . 5 ⊢ (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦)
2	1	a1i 11	. . . 4 ⊢ (𝑥 ∈ Word 𝑉 → (((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥 prefix 𝑁) = 𝑦))
3	2	ss2rabi 4032	. . 3 ⊢ {𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
4	3	rgenw 3083	. 2 ⊢ ∀𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} ⊆ {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
5		disjwrdpfx 14727	. 2 ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
6		disjss2 5075	. 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 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  {crab 3417   ⊆ wss 3907  {cpr 4587  Disj wdisj 5072  ‘cfv 6525  (class class class)co 7400  0cc0 11088  Word cword 14540  lastSclsw 14589   prefix cpfx 14698  Vtxcvtx 29255  Edgcedg 29306   WWalksN cwwlksn 30084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rmo 3370  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-ss 3924  df-disj 5073

This theorem is referenced by: (None)