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

Theorem 2wspmdisj 27512
 Description: The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.)
Hypotheses
Ref Expression
frgrhash2wsp.v 𝑉 = (Vtx‘𝐺)
fusgreg2wsp.m 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
Assertion
Ref Expression
2wspmdisj Disj 𝑥𝑉 (𝑀𝑥)
Distinct variable groups:   𝐺,𝑎   𝑉,𝑎   𝑤,𝐺,𝑎,𝑥   𝑥,𝑉,𝑎,𝑤   𝑥,𝑀   𝑤,𝑉
Allowed substitution hints:   𝑀(𝑤,𝑎)

Proof of Theorem 2wspmdisj
Dummy variables 𝑦 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 orc 399 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
21a1d 25 . . . 4 (𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
3 frgrhash2wsp.v . . . . . . . . . . . . . 14 𝑉 = (Vtx‘𝐺)
4 fusgreg2wsp.m . . . . . . . . . . . . . 14 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
53, 4fusgreg2wsplem 27508 . . . . . . . . . . . . 13 (𝑦𝑉 → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
65adantl 473 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
76adantr 472 . . . . . . . . . . 11 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
83, 4fusgreg2wsplem 27508 . . . . . . . . . . . . . 14 (𝑥𝑉 → (𝑡 ∈ (𝑀𝑥) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥)))
9 eqtr2 2780 . . . . . . . . . . . . . . . . . 18 (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)
109expcom 450 . . . . . . . . . . . . . . . . 17 ((𝑡‘1) = 𝑦 → ((𝑡‘1) = 𝑥𝑥 = 𝑦))
1110adantl 473 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → ((𝑡‘1) = 𝑥𝑥 = 𝑦))
1211com12 32 . . . . . . . . . . . . . . 15 ((𝑡‘1) = 𝑥 → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
1312adantl 473 . . . . . . . . . . . . . 14 ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
148, 13syl6bi 243 . . . . . . . . . . . . 13 (𝑥𝑉 → (𝑡 ∈ (𝑀𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)))
1514adantr 472 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)))
1615imp 444 . . . . . . . . . . 11 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
177, 16sylbid 230 . . . . . . . . . 10 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (𝑡 ∈ (𝑀𝑦) → 𝑥 = 𝑦))
1817con3d 148 . . . . . . . . 9 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦)))
1918impancom 455 . . . . . . . 8 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑡 ∈ (𝑀𝑥) → ¬ 𝑡 ∈ (𝑀𝑦)))
2019ralrimiv 3103 . . . . . . 7 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
21 disj 4160 . . . . . . 7 (((𝑀𝑥) ∩ (𝑀𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
2220, 21sylibr 224 . . . . . 6 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
2322olcd 407 . . . . 5 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2423expcom 450 . . . 4 𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
252, 24pm2.61i 176 . . 3 ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2625rgen2a 3115 . 2 𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
27 fveq2 6353 . . 3 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
2827disjor 4786 . 2 (Disj 𝑥𝑉 (𝑀𝑥) ↔ ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2926, 28mpbir 221 1 Disj 𝑥𝑉 (𝑀𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050  {crab 3054   ∩ cin 3714  ∅c0 4058  Disj wdisj 4772   ↦ cmpt 4881  ‘cfv 6049  (class class class)co 6814  1c1 10149  2c2 11282  Vtxcvtx 26094   WSPathsN cwwspthsn 26952 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6817 This theorem is referenced by:  fusgreghash2wsp  27513
 Copyright terms: Public domain W3C validator