Theorem iswwlksnon 27937

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.)

Hypothesis

Ref	Expression
iswwlksnon.v	⊢ 𝑉 = (Vtx‘𝐺)

Assertion

Ref	Expression
iswwlksnon	⊢ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}

Distinct variable groups:   𝑤,𝐴   𝑤,𝐵   𝑤,𝐺   𝑤,𝑁   𝑤,𝑉

Proof of Theorem iswwlksnon

Dummy variables 𝑎 𝑏 𝑔 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ov 7250	. . 3 ⊢ (𝐴∅𝐵) = ∅
2		df-wwlksnon 27916	. . . . 5 ⊢ WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))
3	2	mpondm0 7446	. . . 4 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝑁 WWalksNOn 𝐺) = ∅)
4	3	oveqd 7230	. . 3 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = (𝐴∅𝐵))
5		df-wwlksn 27915	. . . . . 6 ⊢ WWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})
6	5	mpondm0 7446	. . . . 5 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝑁 WWalksN 𝐺) = ∅)
7	6	rabeqdv 3395	. . . 4 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = {𝑤 ∈ ∅ ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
8		rab0 4297	. . . 4 ⊢ {𝑤 ∈ ∅ ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅
9	7, 8	eqtrdi 2794	. . 3 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅)
10	1, 4, 9	3eqtr4a 2804	. 2 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
11		iswwlksnon.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
12	11	wwlksnon 27935	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)}))
13	12	adantr 484	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ ¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)}))
14	13	oveqd 7230	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ ¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})𝐵))
15		eqid 2737	. . . . . . . 8 ⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})
16	15	mpondm0 7446	. . . . . . 7 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})𝐵) = ∅)
17	16	adantl 485	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ ¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})𝐵) = ∅)
18	14, 17	eqtrd 2777	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ ¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅)
19	18	ex 416	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅))
20	4, 1	eqtrdi 2794	. . . . 5 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅)
21	20	a1d 25	. . . 4 ⊢ (¬ (𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) → (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅))
22	19, 21	pm2.61i 185	. . 3 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅)
23	11	wwlknllvtx 27930	. . . . . . 7 ⊢ (𝑤 ∈ (𝑁 WWalksN 𝐺) → ((𝑤‘0) ∈ 𝑉 ∧ (𝑤‘𝑁) ∈ 𝑉))
24		eleq1 2825	. . . . . . . . 9 ⊢ (𝐴 = (𝑤‘0) → (𝐴 ∈ 𝑉 ↔ (𝑤‘0) ∈ 𝑉))
25	24	eqcoms 2745	. . . . . . . 8 ⊢ ((𝑤‘0) = 𝐴 → (𝐴 ∈ 𝑉 ↔ (𝑤‘0) ∈ 𝑉))
26		eleq1 2825	. . . . . . . . 9 ⊢ (𝐵 = (𝑤‘𝑁) → (𝐵 ∈ 𝑉 ↔ (𝑤‘𝑁) ∈ 𝑉))
27	26	eqcoms 2745	. . . . . . . 8 ⊢ ((𝑤‘𝑁) = 𝐵 → (𝐵 ∈ 𝑉 ↔ (𝑤‘𝑁) ∈ 𝑉))
28	25, 27	bi2anan9 639	. . . . . . 7 ⊢ (((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ↔ ((𝑤‘0) ∈ 𝑉 ∧ (𝑤‘𝑁) ∈ 𝑉)))
29	23, 28	syl5ibrcom 250	. . . . . 6 ⊢ (𝑤 ∈ (𝑁 WWalksN 𝐺) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))
30	29	con3rr3 158	. . . . 5 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑤 ∈ (𝑁 WWalksN 𝐺) → ¬ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)))
31	30	ralrimiv 3104	. . . 4 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ∀𝑤 ∈ (𝑁 WWalksN 𝐺) ¬ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵))
32		rabeq0 4299	. . . 4 ⊢ ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅ ↔ ∀𝑤 ∈ (𝑁 WWalksN 𝐺) ¬ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵))
33	31, 32	sylibr 237	. . 3 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅)
34	22, 33	eqtr4d 2780	. 2 ⊢ (¬ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
35	12	adantr 484	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)}))
36		eqeq2 2749	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝑤‘0) = 𝑎 ↔ (𝑤‘0) = 𝐴))
37		eqeq2 2749	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝑤‘𝑁) = 𝑏 ↔ (𝑤‘𝑁) = 𝐵))
38	36, 37	bi2anan9 639	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏) ↔ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)))
39	38	rabbidv 3390	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
40	39	adantl 485	. . 3 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
41		simprl 771	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐴 ∈ 𝑉)
42		simprr 773	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐵 ∈ 𝑉)
43		ovex 7246	. . . . 5 ⊢ (𝑁 WWalksN 𝐺) ∈ V
44	43	rabex 5225	. . . 4 ⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} ∈ V
45	44	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} ∈ V)
46	35, 40, 41, 42, 45	ovmpod 7361	. 2 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})
47	10, 34, 46	ecase 1033	1 ⊢ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3061  {crab 3065  Vcvv 3408  ∅c0 4237  ‘cfv 6380  (class class class)co 7213   ∈ cmpo 7215  0cc0 10729  1c1 10730   + caddc 10732  ℕ₀cn0 12090  ♯chash 13896  Vtxcvtx 27087  WWalkscwwlks 27909   WWalksN cwwlksn 27910   WWalksNOn cwwlksnon 27911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096  df-fzo 13239  df-hash 13897  df-word 14070  df-wwlks 27914  df-wwlksn 27915  df-wwlksnon 27916

This theorem is referenced by:  wwlknon  27941  wwlksnonfi  28004  wpthswwlks2on  28045  clwwlknclwwlkdif  28062  clwwlknclwwlkdifnum  28063  numclwwlkqhash  28458