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 41501
 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 399 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
21a1d 25 . . . 4 (𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
3 fusgreg2wsp.m . . . . . . . . . . . . . 14 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
43a1i 11 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}))
5 eqeq2 2621 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑥))
65rabbidv 3164 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
76adantl 481 . . . . . . . . . . . . 13 (((𝑥𝑉𝑦𝑉) ∧ 𝑎 = 𝑥) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
8 simpl 472 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → 𝑥𝑉)
9 ovex 6577 . . . . . . . . . . . . . . 15 (2 WSPathsN 𝐺) ∈ V
109rabex 4740 . . . . . . . . . . . . . 14 {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V
1110a1i 11 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V)
124, 7, 8, 11fvmptd 6197 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → (𝑀𝑥) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})
1312eleq2d 2673 . . . . . . . . . . 11 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}))
14 fveq1 6102 . . . . . . . . . . . . . 14 (𝑤 = 𝑡 → (𝑤‘1) = (𝑡‘1))
1514eqeq1d 2612 . . . . . . . . . . . . 13 (𝑤 = 𝑡 → ((𝑤‘1) = 𝑥 ↔ (𝑡‘1) = 𝑥))
1615elrab 3331 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥))
17 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑦 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑦))
1817rabbidv 3164 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑦 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
1918adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝑉𝑦𝑉) ∧ 𝑎 = 𝑦) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
20 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑉𝑦𝑉) → 𝑦𝑉)
219rabex 4740 . . . . . . . . . . . . . . . . . . . . 21 {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V
2221a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑉𝑦𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V)
234, 19, 20, 22fvmptd 6197 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑉𝑦𝑉) → (𝑀𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
2423adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑀𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})
2524eleq2d 2673 . . . . . . . . . . . . . . . . 17 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}))
2614eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → ((𝑤‘1) = 𝑦 ↔ (𝑡‘1) = 𝑦))
2726elrab 3331 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))
2825, 27syl6bb 275 . . . . . . . . . . . . . . . 16 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)))
29 eqtr2 2630 . . . . . . . . . . . . . . . . . . 19 (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)
3029ex 449 . . . . . . . . . . . . . . . . . 18 ((𝑡‘1) = 𝑥 → ((𝑡‘1) = 𝑦𝑥 = 𝑦))
3130adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡‘1) = 𝑦𝑥 = 𝑦))
3231adantld 482 . . . . . . . . . . . . . . . 16 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))
3328, 32sylbid 229 . . . . . . . . . . . . . . 15 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀𝑦) → 𝑥 = 𝑦))
3433con3d 147 . . . . . . . . . . . . . 14 (((𝑥𝑉𝑦𝑉) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦)))
3534ex 449 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → ((𝑡‘1) = 𝑥 → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3635adantld 482 . . . . . . . . . . . 12 ((𝑥𝑉𝑦𝑉) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3716, 36syl5bi 231 . . . . . . . . . . 11 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3813, 37sylbid 229 . . . . . . . . . 10 ((𝑥𝑉𝑦𝑉) → (𝑡 ∈ (𝑀𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀𝑦))))
3938com23 84 . . . . . . . . 9 ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → (𝑡 ∈ (𝑀𝑥) → ¬ 𝑡 ∈ (𝑀𝑦))))
4039imp31 447 . . . . . . . 8 ((((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ 𝑡 ∈ (𝑀𝑦))
4140ralrimiva 2949 . . . . . . 7 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
42 disj 3969 . . . . . . 7 (((𝑀𝑥) ∩ (𝑀𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
4341, 42sylibr 223 . . . . . 6 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
4443olcd 407 . . . . 5 (((𝑥𝑉𝑦𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
4544expcom 450 . . . 4 𝑥 = 𝑦 → ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
462, 45pm2.61i 175 . . 3 ((𝑥𝑉𝑦𝑉) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
4746rgen2 2958 . 2 𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
48 fveq2 6103 . . 3 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
4948disjor 4567 . 2 (Disj 𝑥𝑉 (𝑀𝑥) ↔ ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
5047, 49mpbir 220 1 Disj 𝑥𝑉 (𝑀𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173   ∩ cin 3539  ∅c0 3874  Disj wdisj 4553   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  1c1 9816  2c2 10947  Vtxcvtx 25673   WSPathsN cwwspthsn 41031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552 This theorem is referenced by:  fusgreghash2wsp  41502
 Copyright terms: Public domain W3C validator