Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2wspmdisj Structured version   Visualization version   GIF version

Theorem 2wspmdisj 41482
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.)
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 398 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
21a1d 25 . . . 4 (𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
3 fusgreg2wsp.m . . . . . . . . . . . . . 14 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
43a1i 11 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}))
5 eqeq2 2620 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑥))
65rabbidv 3163 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
76adantl 480 . . . . . . . . . . . . 13 (((𝑥𝑉𝑦𝑉) ∧ 𝑎 = 𝑥) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
8 simpl 471 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → 𝑥𝑉)
9 ovex 6554 . . . . . . . . . . . . . . 15 (2 WSPathsN 𝐺) ∈ V
109rabex 4734 . . . . . . . . . . . . . 14 {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V
1110a1i 11 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V)
124, 7, 8, 11fvmptd 6181 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑀𝑥) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
1312eleq2d 2672 . . . . . . . . . . 11 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}))
14 fveq1 6086 . . . . . . . . . . . . . 14 (𝑤 = 𝑡 → (𝑤‘1) = (𝑡‘1))
1514eqeq1d 2611 . . . . . . . . . . . . 13 (𝑤 = 𝑡 → ((𝑤‘1) = 𝑥 ↔ (𝑡‘1) = 𝑥))
1615elrab 3330 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥))
17 eqeq2 2620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑦 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑦))
1817rabbidv 3163 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑦 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
1918adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝑉𝑦𝑉) ∧ 𝑎 = 𝑦) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
20 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑉𝑦𝑉) → 𝑦𝑉)
219rabex 4734 . . . . . . . . . . . . . . . . . . . . 21 {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V
2221a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑉𝑦𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V)
234, 19, 20, 22fvmptd 6181 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑉𝑦𝑉) → (𝑀𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
2423adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑀𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
2524eleq2d 2672 . . . . . . . . . . . . . . . . 17 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}))
2614eqeq1d 2611 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → ((𝑤‘1) = 𝑦 ↔ (𝑡‘1) = 𝑦))
2726elrab 3330 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))
2825, 27syl6bb 274 . . . . . . . . . . . . . . . 16 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
29 eqtr2 2629 . . . . . . . . . . . . . . . . . . 19 (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)
3029ex 448 . . . . . . . . . . . . . . . . . 18 ((𝑡‘1) = 𝑥 → ((𝑡‘1) = 𝑦𝑥 = 𝑦))
3130adantl 480 . . . . . . . . . . . . . . . . 17 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡‘1) = 𝑦𝑥 = 𝑦))
3231adantld 481 . . . . . . . . . . . . . . . 16 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
3328, 32sylbid 228 . . . . . . . . . . . . . . 15 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) → 𝑥 = 𝑦))
3433con3d 146 . . . . . . . . . . . . . 14 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦)))
3534ex 448 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → ((𝑡‘1) = 𝑥 → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3635adantld 481 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3716, 36syl5bi 230 . . . . . . . . . . 11 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3813, 37sylbid 228 . . . . . . . . . 10 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3938com23 83 . . . . . . . . 9 ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → (𝑡 ∈ (𝑀𝑥) → ¬ 𝑡 ∈ (𝑀𝑦))))
4039imp31 446 . . . . . . . 8 ((((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ 𝑡 ∈ (𝑀𝑦))
4140ralrimiva 2948 . . . . . . 7 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
42 disj 3968 . . . . . . 7 (((𝑀𝑥) ∩ (𝑀𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
4341, 42sylibr 222 . . . . . 6 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
4443olcd 406 . . . . 5 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
4544expcom 449 . . . 4 𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
462, 45pm2.61i 174 . . 3 ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
4746rgen2 2957 . 2 𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
48 fveq2 6087 . . 3 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
4948disjor 4561 . 2 (Disj 𝑥𝑉 (𝑀𝑥) ↔ ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
5047, 49mpbir 219 1 Disj 𝑥𝑉 (𝑀𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381  wa 382   = wceq 1474  wcel 1976  wral 2895  {crab 2899  Vcvv 3172  cin 3538  c0 3873  Disj wdisj 4547  cmpt 4637  cfv 5789  (class class class)co 6526  1c1 9793  2c2 10919  Vtxcvtx 40210   WSPathsN cwwspthsn 41012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-iota 5753  df-fun 5791  df-fv 5797  df-ov 6529
This theorem is referenced by:  fusgreghash2wsp  41483
  Copyright terms: Public domain W3C validator