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

Theorem 2clwwlk2 29396
Description: The set (𝑋𝐶2) of double loops of length 2 on a vertex 𝑋 is equal to the set of closed walks with length 2 on 𝑋. Considered as "double loops", the first of the two closed walks/loops is degenerated, i.e., has length 0. (Contributed by AV, 18-Feb-2022.) (Revised by AV, 20-Apr-2022.)
Hypothesis
Ref Expression
2clwwlk.c 𝐶 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
Assertion
Ref Expression
2clwwlk2 (𝑋𝑉 → (𝑋𝐶2) = (𝑋(ClWWalksNOn‘𝐺)2))
Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑉,𝑣   𝑛,𝑋,𝑣,𝑤
Allowed substitution hints:   𝐶(𝑤,𝑣,𝑛)   𝑉(𝑤)

Proof of Theorem 2clwwlk2
StepHypRef Expression
1 2z 12566 . . . 4 2 ∈ ℤ
2 uzid 12809 . . . 4 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
31, 2ax-mp 5 . . 3 2 ∈ (ℤ‘2)
4 2clwwlk.c . . . 4 𝐶 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
542clwwlk 29395 . . 3 ((𝑋𝑉 ∧ 2 ∈ (ℤ‘2)) → (𝑋𝐶2) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∣ (𝑤‘(2 − 2)) = 𝑋})
63, 5mpan2 689 . 2 (𝑋𝑉 → (𝑋𝐶2) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∣ (𝑤‘(2 − 2)) = 𝑋})
7 2cn 12259 . . . . . 6 2 ∈ ℂ
87subidi 11503 . . . . 5 (2 − 2) = 0
98fveq2i 6872 . . . 4 (𝑤‘(2 − 2)) = (𝑤‘0)
10 isclwwlknon 29139 . . . . 5 (𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) ↔ (𝑤 ∈ (2 ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋))
1110simprbi 497 . . . 4 (𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) → (𝑤‘0) = 𝑋)
129, 11eqtrid 2783 . . 3 (𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) → (𝑤‘(2 − 2)) = 𝑋)
1312rabeqc 3437 . 2 {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∣ (𝑤‘(2 − 2)) = 𝑋} = (𝑋(ClWWalksNOn‘𝐺)2)
146, 13eqtrdi 2787 1 (𝑋𝑉 → (𝑋𝐶2) = (𝑋(ClWWalksNOn‘𝐺)2))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  {crab 3425  cfv 6523  (class class class)co 7384  cmpo 7386  0cc0 11082  cmin 11416  2c2 12239  cz 12530  cuz 12794   ClWWalksN cclwwlkn 29072  ClWWalksNOncclwwlknon 29135
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5269  ax-sep 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699  ax-cnex 11138  ax-resscn 11139  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-addrcl 11143  ax-mulcl 11144  ax-mulrcl 11145  ax-mulcom 11146  ax-addass 11147  ax-mulass 11148  ax-distr 11149  ax-i2m1 11150  ax-1ne0 11151  ax-1rid 11152  ax-rnegex 11153  ax-rrecex 11154  ax-cnre 11155  ax-pre-lttri 11156  ax-pre-lttrn 11157  ax-pre-ltadd 11158  ax-pre-mulgt0 11159
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-pss 3954  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-int 4935  df-iun 4983  df-br 5133  df-opab 5195  df-mpt 5216  df-tr 5250  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5615  df-we 5617  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6280  df-ord 6347  df-on 6348  df-lim 6349  df-suc 6350  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7340  df-ov 7387  df-oprab 7388  df-mpo 7389  df-om 7830  df-1st 7948  df-2nd 7949  df-frecs 8239  df-wrecs 8270  df-recs 8344  df-rdg 8383  df-1o 8439  df-oadd 8443  df-er 8677  df-map 8796  df-en 8913  df-dom 8914  df-sdom 8915  df-fin 8916  df-card 9906  df-pnf 11222  df-mnf 11223  df-xr 11224  df-ltxr 11225  df-le 11226  df-sub 11418  df-neg 11419  df-nn 12185  df-2 12247  df-n0 12445  df-xnn0 12517  df-z 12531  df-uz 12795  df-fz 13457  df-fzo 13600  df-hash 14263  df-word 14437  df-clwwlk 29030  df-clwwlkn 29073  df-clwwlknon 29136
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator