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

Theorem 2wspmdisj 27685
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 894 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
21a1d 25 . . . 4 (𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
3 frgrhash2wsp.v . . . . . . . . . . . . . 14 𝑉 = (Vtx‘𝐺)
4 fusgreg2wsp.m . . . . . . . . . . . . . 14 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
53, 4fusgreg2wsplem 27681 . . . . . . . . . . . . 13 (𝑦𝑉 → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
65adantl 474 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
76adantr 473 . . . . . . . . . . 11 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
83, 4fusgreg2wsplem 27681 . . . . . . . . . . . . . 14 (𝑥𝑉 → (𝑡 ∈ (𝑀𝑥) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥)))
9 eqtr2 2820 . . . . . . . . . . . . . . . . . 18 (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)
109expcom 403 . . . . . . . . . . . . . . . . 17 ((𝑡‘1) = 𝑦 → ((𝑡‘1) = 𝑥𝑥 = 𝑦))
1110adantl 474 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → ((𝑡‘1) = 𝑥𝑥 = 𝑦))
1211com12 32 . . . . . . . . . . . . . . 15 ((𝑡‘1) = 𝑥 → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
1312adantl 474 . . . . . . . . . . . . . 14 ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
148, 13syl6bi 245 . . . . . . . . . . . . 13 (𝑥𝑉 → (𝑡 ∈ (𝑀𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)))
1514adantr 473 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)))
1615imp 396 . . . . . . . . . . 11 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
177, 16sylbid 232 . . . . . . . . . 10 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (𝑡 ∈ (𝑀𝑦) → 𝑥 = 𝑦))
1817con3d 150 . . . . . . . . 9 (((𝑥𝑉𝑦𝑉) ∧ 𝑡 ∈ (𝑀𝑥)) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦)))
1918impancom 444 . . . . . . . 8 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑡 ∈ (𝑀𝑥) → ¬ 𝑡 ∈ (𝑀𝑦)))
2019ralrimiv 3147 . . . . . . 7 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
21 disj 4213 . . . . . . 7 (((𝑀𝑥) ∩ (𝑀𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
2220, 21sylibr 226 . . . . . 6 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
2322olcd 901 . . . . 5 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2423expcom 403 . . . 4 𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
252, 24pm2.61i 177 . . 3 ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2625rgen2a 3159 . 2 𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
27 fveq2 6412 . . 3 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
2827disjor 4826 . 2 (Disj 𝑥𝑉 (𝑀𝑥) ↔ ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
2926, 28mpbir 223 1 Disj 𝑥𝑉 (𝑀𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wo 874   = wceq 1653  wcel 2157  wral 3090  {crab 3094  cin 3769  c0 4116  Disj wdisj 4812  cmpt 4923  cfv 6102  (class class class)co 6879  1c1 10226  2c2 11367  Vtxcvtx 26230   WSPathsN cwwspthsn 27078
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-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pr 5098
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rmo 3098  df-rab 3099  df-v 3388  df-sbc 3635  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-disj 4813  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-iota 6065  df-fun 6104  df-fv 6110  df-ov 6882
This theorem is referenced by:  fusgreghash2wsp  27686
  Copyright terms: Public domain W3C validator