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-onto→wf1o 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