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

Theorem 2spotmdisj 26595
 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, 17-Sep-2021.)
Hypothesis
Ref Expression
usgreghash2spot.m 𝑀 = (𝑎𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎)})
Assertion
Ref Expression
2spotmdisj (𝑉𝑊Disj 𝑥𝑉 (𝑀𝑥))
Distinct variable groups:   𝑡,𝐸,𝑥,𝑎   𝑉,𝑎,𝑡,𝑥   𝐸,𝑎   𝑡,𝑀,𝑥   𝑡,𝑊,𝑥
Allowed substitution hints:   𝑀(𝑎)   𝑊(𝑎)

Proof of Theorem 2spotmdisj
Dummy variables 𝑦 𝑐 𝑑 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 orc 399 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
21a1d 25 . . . 4 (𝑥 = 𝑦 → ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
3 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑥𝑉𝑦𝑉) → 𝑥𝑉)
4 3xpexg 6859 . . . . . . . . . . . . . . . . 17 (𝑉𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V)
5 rabexg 4739 . . . . . . . . . . . . . . . . 17 (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)} ∈ V)
64, 5syl 17 . . . . . . . . . . . . . . . 16 (𝑉𝑊 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)} ∈ V)
7 eqeq2 2621 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → ((2nd ‘(1st𝑡)) = 𝑎 ↔ (2nd ‘(1st𝑡)) = 𝑥))
87anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑥 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)))
98rabbidv 3164 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑥 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)})
10 usgreghash2spot.m . . . . . . . . . . . . . . . . 17 𝑀 = (𝑎𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎)})
119, 10fvmptg 6189 . . . . . . . . . . . . . . . 16 ((𝑥𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)} ∈ V) → (𝑀𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)})
123, 6, 11syl2anr 494 . . . . . . . . . . . . . . 15 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑀𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)})
1312eleq2d 2673 . . . . . . . . . . . . . 14 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑡 ∈ (𝑀𝑥) ↔ 𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)}))
14 rabid 3095 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)} ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)))
15 el2xptp 7102 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ↔ ∃𝑏𝑉𝑐𝑉𝑑𝑉 𝑡 = ⟨𝑏, 𝑐, 𝑑⟩)
16 ot2ndg 7074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑉𝑐𝑉𝑑𝑉) → (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑐)
17163expa 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑐)
1817eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑥𝑐 = 𝑥))
1917adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) ∧ 𝑐 = 𝑥) → (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑐)
2019eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) ∧ 𝑐 = 𝑥) → ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦𝑐 = 𝑦))
21 ax7 1930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → (𝑐 = 𝑦𝑥 = 𝑦))
2221adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) ∧ 𝑐 = 𝑥) → (𝑐 = 𝑦𝑥 = 𝑦))
2320, 22sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) ∧ 𝑐 = 𝑥) → ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦𝑥 = 𝑦))
2423con3d 147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) ∧ 𝑐 = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))
2524ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → (𝑐 = 𝑥 → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦)))
2625a1dd 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → (𝑐 = 𝑥 → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))))
2718, 26sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑥 → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))))
2827com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑥 → (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))))
2928a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑥 → (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦)))))
30 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (1st𝑡) = (1st ‘⟨𝑏, 𝑐, 𝑑⟩))
3130fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (2nd ‘(1st𝑡)) = (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)))
3231eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((2nd ‘(1st𝑡)) = 𝑥 ↔ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑥))
3331eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((2nd ‘(1st𝑡)) = 𝑦 ↔ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))
3433notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (¬ (2nd ‘(1st𝑡)) = 𝑦 ↔ ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))
3534imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦) ↔ (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦)))
3635imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)) ↔ ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦))))
3736imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦))) ↔ (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st ‘⟨𝑏, 𝑐, 𝑑⟩)) = 𝑦)))))
3829, 32, 373imtr4d 282 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((2nd ‘(1st𝑡)) = 𝑥 → (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))))
3938com12 32 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ‘(1st𝑡)) = 𝑥 → (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))))
4039adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥) → (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))))
4140com13 86 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑉𝑐𝑉) ∧ 𝑑𝑉) → (𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))))
4241rexlimdva 3013 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑉𝑐𝑉) → (∃𝑑𝑉 𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))))
4342rexlimivv 3018 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝑉𝑐𝑉𝑑𝑉 𝑡 = ⟨𝑏, 𝑐, 𝑑⟩ → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦))))
4415, 43sylbi 206 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦))))
4544imp 444 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)) → ((𝑥𝑉𝑦𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
4645com12 32 . . . . . . . . . . . . . . . 16 ((𝑥𝑉𝑦𝑉) → ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
4746adantl 481 . . . . . . . . . . . . . . 15 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
4814, 47syl5bi 231 . . . . . . . . . . . . . 14 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑥)} → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
4913, 48sylbid 229 . . . . . . . . . . . . 13 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑡 ∈ (𝑀𝑥) → (¬ 𝑥 = 𝑦 → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
5049com23 84 . . . . . . . . . . . 12 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (¬ 𝑥 = 𝑦 → (𝑡 ∈ (𝑀𝑥) → ¬ (2nd ‘(1st𝑡)) = 𝑦)))
5150imp31 447 . . . . . . . . . . 11 ((((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ (2nd ‘(1st𝑡)) = 𝑦)
5251intnand 953 . . . . . . . . . 10 ((((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦))
5352intnand 953 . . . . . . . . 9 ((((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)))
54 simpr 476 . . . . . . . . . . . . . . 15 ((𝑥𝑉𝑦𝑉) → 𝑦𝑉)
55 rabexg 4739 . . . . . . . . . . . . . . . 16 (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)} ∈ V)
564, 55syl 17 . . . . . . . . . . . . . . 15 (𝑉𝑊 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)} ∈ V)
57 eqeq2 2621 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑦 → ((2nd ‘(1st𝑡)) = 𝑎 ↔ (2nd ‘(1st𝑡)) = 𝑦))
5857anbi2d 736 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑦 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)))
5958rabbidv 3164 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)})
6059, 10fvmptg 6189 . . . . . . . . . . . . . . 15 ((𝑦𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)} ∈ V) → (𝑀𝑦) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)})
6154, 56, 60syl2anr 494 . . . . . . . . . . . . . 14 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑀𝑦) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)})
6261eleq2d 2673 . . . . . . . . . . . . 13 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑡 ∈ (𝑀𝑦) ↔ 𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)}))
63 rabid 3095 . . . . . . . . . . . . 13 (𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)} ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦)))
6462, 63syl6bb 275 . . . . . . . . . . . 12 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑡 ∈ (𝑀𝑦) ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦))))
6564notbid 307 . . . . . . . . . . 11 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (¬ 𝑡 ∈ (𝑀𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦))))
6665adantr 480 . . . . . . . . . 10 (((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) → (¬ 𝑡 ∈ (𝑀𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦))))
6766adantr 480 . . . . . . . . 9 ((((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → (¬ 𝑡 ∈ (𝑀𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st𝑡)) = 𝑦))))
6853, 67mpbird 246 . . . . . . . 8 ((((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀𝑥)) → ¬ 𝑡 ∈ (𝑀𝑦))
6968ralrimiva 2949 . . . . . . 7 (((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
70 disj 3969 . . . . . . 7 (((𝑀𝑥) ∩ (𝑀𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀𝑥) ¬ 𝑡 ∈ (𝑀𝑦))
7169, 70sylibr 223 . . . . . 6 (((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) → ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)
7271olcd 407 . . . . 5 (((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
7372expcom 450 . . . 4 𝑥 = 𝑦 → ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅)))
742, 73pm2.61i 175 . . 3 ((𝑉𝑊 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
7574ralrimivva 2954 . 2 (𝑉𝑊 → ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
76 fveq2 6103 . . 3 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
7776disjor 4567 . 2 (Disj 𝑥𝑉 (𝑀𝑥) ↔ ∀𝑥𝑉𝑦𝑉 (𝑥 = 𝑦 ∨ ((𝑀𝑥) ∩ (𝑀𝑦)) = ∅))
7875, 77sylibr 223 1 (𝑉𝑊Disj 𝑥𝑉 (𝑀𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∩ cin 3539  ∅c0 3874  ⟨cotp 4133  Disj wdisj 4553   ↦ cmpt 4643   × cxp 5036  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   2SPathsOt c2spthot 26383 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-8 1979  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-pow 4769  ax-pr 4833  ax-un 6847 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-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-ot 4134  df-uni 4373  df-iun 4457  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-rn 5049  df-iota 5768  df-fun 5806  df-fv 5812  df-1st 7059  df-2nd 7060 This theorem is referenced by:  usgreghash2spot  26596
 Copyright terms: Public domain W3C validator