Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
3 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
4 | | 3xpexg 6859 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V) |
5 | | rabexg 4739 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ 𝑊 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) |
7 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑥 → ((2nd
‘(1st ‘𝑡)) = 𝑎 ↔ (2nd
‘(1st ‘𝑡)) = 𝑥)) |
8 | 7 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑥 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥))) |
9 | 8 | rabbidv 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑥 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
10 | | usgreghash2spot.m |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)}) |
11 | 9, 10 | fvmptg 6189 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) → (𝑀‘𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
12 | 3, 6, 11 | syl2anr 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑀‘𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
13 | 12 | eleq2d 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 ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑐) |
17 | 16 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑐) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑥 ↔ 𝑐 = 𝑥)) |
19 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 = 𝑥) → (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑐) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 = 𝑥) → ((2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦 ↔ 𝑐 = 𝑦)) |
21 | | ax7 1930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑥 → (𝑐 = 𝑦 → 𝑥 = 𝑦)) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 = 𝑥) → (𝑐 = 𝑦 → 𝑥 = 𝑦)) |
23 | 20, 22 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 = 𝑥) → ((2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦 → 𝑥 = 𝑦)) |
24 | 23 | con3d 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑐 = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)) |
25 | 24 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑐 = 𝑥 → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦))) |
26 | 25 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑐 = 𝑥 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)))) |
27 | 18, 26 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑥 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)))) |
28 | 27 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((2nd ‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑥 → (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)))) |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑥 → (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦))))) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (1st ‘𝑡) = (1st
‘〈𝑏, 𝑐, 𝑑〉)) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘〈𝑏, 𝑐, 𝑑〉))) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((2nd
‘(1st ‘𝑡)) = 𝑥 ↔ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑥)) |
33 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((2nd
‘(1st ‘𝑡)) = 𝑦 ↔ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)) |
34 | 33 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (¬ (2nd
‘(1st ‘𝑡)) = 𝑦 ↔ ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)) |
35 | 34 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦) ↔ (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦))) |
36 | 35 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦)) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦)))) |
37 | 36 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) ↔ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘〈𝑏, 𝑐, 𝑑〉)) = 𝑦))))) |
38 | 29, 32, 37 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((2nd
‘(1st ‘𝑡)) = 𝑥 → (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))))) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((2nd ‘(1st ‘𝑡)) = 𝑥 → (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))))) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) → (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))))) |
41 | 40 | com13 86 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))))) |
42 | 41 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (∃𝑑 ∈ 𝑉 𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))))) |
43 | 42 | rexlimivv 3018 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 𝑡 = 〈𝑏, 𝑐, 𝑑〉 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
44 | 15, 43 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
45 | 44 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
48 | 14, 47 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
49 | 13, 48 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑡 ∈ (𝑀‘𝑥) → (¬ 𝑥 = 𝑦 → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
50 | 49 | com23 84 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (¬ 𝑥 = 𝑦 → (𝑡 ∈ (𝑀‘𝑥) → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
51 | 50 | imp31 447 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ¬ (2nd
‘(1st ‘𝑡)) = 𝑦) |
52 | 51 | intnand 953 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ¬ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)) |
53 | 52 | intnand 953 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
54 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
55 | | rabexg 4739 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)} ∈ V) |
56 | 4, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ 𝑊 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)} ∈ V) |
57 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑦 → ((2nd
‘(1st ‘𝑡)) = 𝑎 ↔ (2nd
‘(1st ‘𝑡)) = 𝑦)) |
58 | 57 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑦 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
59 | 58 | rabbidv 3164 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑦 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)}) |
60 | 59, 10 | fvmptg 6189 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)} ∈ V) → (𝑀‘𝑦) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)}) |
61 | 54, 56, 60 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑀‘𝑦) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)}) |
62 | 61 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑡 ∈ (𝑀‘𝑦) ↔ 𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)})) |
63 | | rabid 3095 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)} ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦))) |
64 | 62, 63 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
65 | 64 | notbid 307 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (¬ 𝑡 ∈ (𝑀‘𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
66 | 65 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) → (¬ 𝑡 ∈ (𝑀‘𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
67 | 66 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (¬ 𝑡 ∈ (𝑀‘𝑦) ↔ ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑦)))) |
68 | 53, 67 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ¬ 𝑡 ∈ (𝑀‘𝑦)) |
69 | 68 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
70 | | disj 3969 |
. . . . . . 7
⊢ (((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
71 | 69, 70 | sylibr 223 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) → ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) |
72 | 71 | olcd 407 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
73 | 72 | expcom 450 |
. . . 4
⊢ (¬
𝑥 = 𝑦 → ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
74 | 2, 73 | pm2.61i 175 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
75 | 74 | ralrimivva 2954 |
. 2
⊢ (𝑉 ∈ 𝑊 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
76 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) |
77 | 76 | disjor 4567 |
. 2
⊢
(Disj 𝑥
∈ 𝑉 (𝑀‘𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
78 | 75, 77 | sylibr 223 |
1
⊢ (𝑉 ∈ 𝑊 → Disj 𝑥 ∈ 𝑉 (𝑀‘𝑥)) |