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

Theorem dlwwlknondlwlknonf1oOLD 27730
Description: Obsolete version of dlwwlknondlwlknonf1o 27729 as of 12-Oct-2022. (Contributed by AV, 30-May-2022.) (Proof shortened by AV, 8-Aug-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
dlwwlknondlwlknonbij.v 𝑉 = (Vtx‘𝐺)
dlwwlknondlwlknonbij.w 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
dlwwlknondlwlknonbij.d 𝐷 = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}
dlwwlknondlwlknonf1oOLD.f 𝐹 = (𝑐𝑊 ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩))
Assertion
Ref Expression
dlwwlknondlwlknonf1oOLD ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → 𝐹:𝑊1-1-onto𝐷)
Distinct variable groups:   𝐺,𝑐,𝑤   𝑁,𝑐,𝑤   𝑉,𝑐   𝑊,𝑐   𝑋,𝑐,𝑤
Allowed substitution hints:   𝐷(𝑤,𝑐)   𝐹(𝑤,𝑐)   𝑉(𝑤)   𝑊(𝑤)

Proof of Theorem dlwwlknondlwlknonf1oOLD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dlwwlknondlwlknonbij.w . . . 4 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
2 df-3an 1110 . . . . 5 (((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋) ↔ (((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋) ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋))
32rabbii 3368 . . . 4 {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)} = {𝑤 ∈ (ClWalks‘𝐺) ∣ (((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋) ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
41, 3eqtri 2820 . . 3 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋) ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
5 eqid 2798 . . 3 {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)}
6 dlwwlknondlwlknonf1oOLD.f . . 3 𝐹 = (𝑐𝑊 ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩))
7 eqid 2798 . . 3 (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩))
8 eluz2nn 11967 . . . 4 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ)
9 dlwwlknondlwlknonbij.v . . . . 5 𝑉 = (Vtx‘𝐺)
109, 5, 7clwwlknonclwlknonf1oOLD 27724 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)):{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁))
118, 10syl3an3 1206 . . 3 ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ↦ ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)):{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁))
12 fveq1 6409 . . . . . . 7 (𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩) → (𝑦‘(𝑁 − 2)) = (((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)‘(𝑁 − 2)))
13123ad2ant3 1166 . . . . . 6 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) → (𝑦‘(𝑁 − 2)) = (((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)‘(𝑁 − 2)))
14 2fveq3 6415 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (♯‘(1st𝑤)) = (♯‘(1st𝑐)))
1514eqeq1d 2800 . . . . . . . . . . . 12 (𝑤 = 𝑐 → ((♯‘(1st𝑤)) = 𝑁 ↔ (♯‘(1st𝑐)) = 𝑁))
16 fveq2 6410 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → (2nd𝑤) = (2nd𝑐))
1716fveq1d 6412 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → ((2nd𝑤)‘0) = ((2nd𝑐)‘0))
1817eqeq1d 2800 . . . . . . . . . . . 12 (𝑤 = 𝑐 → (((2nd𝑤)‘0) = 𝑋 ↔ ((2nd𝑐)‘0) = 𝑋))
1915, 18anbi12d 625 . . . . . . . . . . 11 (𝑤 = 𝑐 → (((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋) ↔ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)))
2019elrab 3555 . . . . . . . . . 10 (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)))
21 simplrl 796 . . . . . . . . . . . 12 (((𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2))) → (♯‘(1st𝑐)) = 𝑁)
22 simpll 784 . . . . . . . . . . . 12 (((𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2))) → 𝑐 ∈ (ClWalks‘𝐺))
23 simpr3 1253 . . . . . . . . . . . 12 (((𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2))) → 𝑁 ∈ (ℤ‘2))
2421, 22, 233jca 1159 . . . . . . . . . . 11 (((𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2))) → ((♯‘(1st𝑐)) = 𝑁𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ‘2)))
2524ex 402 . . . . . . . . . 10 ((𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st𝑐)) = 𝑁 ∧ ((2nd𝑐)‘0) = 𝑋)) → ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → ((♯‘(1st𝑐)) = 𝑁𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ‘2))))
2620, 25sylbi 209 . . . . . . . . 9 (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} → ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → ((♯‘(1st𝑐)) = 𝑁𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ‘2))))
2726impcom 397 . . . . . . . 8 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)}) → ((♯‘(1st𝑐)) = 𝑁𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ‘2)))
28 dlwwlknonclwlknonf1olem1OLD 27728 . . . . . . . 8 (((♯‘(1st𝑐)) = 𝑁𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ‘2)) → (((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)‘(𝑁 − 2)) = ((2nd𝑐)‘(𝑁 − 2)))
2927, 28syl 17 . . . . . . 7 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)}) → (((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)‘(𝑁 − 2)) = ((2nd𝑐)‘(𝑁 − 2)))
30293adant3 1163 . . . . . 6 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) → (((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)‘(𝑁 − 2)) = ((2nd𝑐)‘(𝑁 − 2)))
3113, 30eqtrd 2832 . . . . 5 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) → (𝑦‘(𝑁 − 2)) = ((2nd𝑐)‘(𝑁 − 2)))
3231eqeq1d 2800 . . . 4 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) → ((𝑦‘(𝑁 − 2)) = 𝑋 ↔ ((2nd𝑐)‘(𝑁 − 2)) = 𝑋))
33 nfv 2010 . . . . 5 𝑤((2nd𝑐)‘(𝑁 − 2)) = 𝑋
3416fveq1d 6412 . . . . . 6 (𝑤 = 𝑐 → ((2nd𝑤)‘(𝑁 − 2)) = ((2nd𝑐)‘(𝑁 − 2)))
3534eqeq1d 2800 . . . . 5 (𝑤 = 𝑐 → (((2nd𝑤)‘(𝑁 − 2)) = 𝑋 ↔ ((2nd𝑐)‘(𝑁 − 2)) = 𝑋))
3633, 35sbie 2525 . . . 4 ([𝑐 / 𝑤]((2nd𝑤)‘(𝑁 − 2)) = 𝑋 ↔ ((2nd𝑐)‘(𝑁 − 2)) = 𝑋)
3732, 36syl6bbr 281 . . 3 (((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd𝑐) substr ⟨0, (♯‘(1st𝑐))⟩)) → ((𝑦‘(𝑁 − 2)) = 𝑋 ↔ [𝑐 / 𝑤]((2nd𝑤)‘(𝑁 − 2)) = 𝑋))
384, 5, 6, 7, 11, 37f1ossf1o 6621 . 2 ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → 𝐹:𝑊1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋})
39 dlwwlknondlwlknonbij.d . . . 4 𝐷 = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}
40 fveq1 6409 . . . . . 6 (𝑤 = 𝑦 → (𝑤‘(𝑁 − 2)) = (𝑦‘(𝑁 − 2)))
4140eqeq1d 2800 . . . . 5 (𝑤 = 𝑦 → ((𝑤‘(𝑁 − 2)) = 𝑋 ↔ (𝑦‘(𝑁 − 2)) = 𝑋))
4241cbvrabv 3382 . . . 4 {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋}
4339, 42eqtri 2820 . . 3 𝐷 = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋}
44 f1oeq3 6346 . . 3 (𝐷 = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋} → (𝐹:𝑊1-1-onto𝐷𝐹:𝑊1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋}))
4543, 44ax-mp 5 . 2 (𝐹:𝑊1-1-onto𝐷𝐹:𝑊1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋})
4638, 45sylibr 226 1 ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → 𝐹:𝑊1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  [wsb 2064  wcel 2157  {crab 3092  cop 4373  cmpt 4921  1-1-ontowf1o 6099  cfv 6100  (class class class)co 6877  1st c1st 7398  2nd c2nd 7399  0cc0 10223  cmin 10555  cn 11311  2c2 11365  cuz 11927  chash 13367   substr csubstr 13661  Vtxcvtx 26224  USPGraphcuspgr 26377  ClWalkscclwlks 27017  ClWWalksNOncclwwlknon 27416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-ifp 1087  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-int 4667  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7400  df-2nd 7401  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-1o 7798  df-2o 7799  df-oadd 7802  df-er 7981  df-map 8096  df-pm 8097  df-en 8195  df-dom 8196  df-sdom 8197  df-fin 8198  df-card 9050  df-cda 9277  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-nn 11312  df-2 11373  df-n0 11578  df-xnn0 11650  df-z 11664  df-uz 11928  df-rp 12072  df-fz 12578  df-fzo 12718  df-hash 13368  df-word 13532  df-lsw 13580  df-concat 13588  df-s1 13613  df-substr 13662  df-pfx 13711  df-edg 26276  df-uhgr 26286  df-upgr 26310  df-uspgr 26379  df-wlks 26842  df-clwlks 27018  df-clwwlk 27268  df-clwwlkn 27321  df-clwwlknon 27417
This theorem is referenced by:  dlwwlknondlwlknonenOLD  27732
  Copyright terms: Public domain W3C validator