Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
3 | | fusgreg2wsp.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
4 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})) |
5 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑥)) |
6 | 5 | rabbidv 3164 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑥 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
7 | 6 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑎 = 𝑥) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
8 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
9 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (2
WSPathsN 𝐺) ∈
V |
10 | 9 | rabex 4740 |
. . . . . . . . . . . . . 14
⊢ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V |
11 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V) |
12 | 4, 7, 8, 11 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑀‘𝑥) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
13 | 12 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑥) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})) |
14 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑡 → (𝑤‘1) = (𝑡‘1)) |
15 | 14 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑡 → ((𝑤‘1) = 𝑥 ↔ (𝑡‘1) = 𝑥)) |
16 | 15 | elrab 3331 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥)) |
17 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑦 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑦)) |
18 | 17 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑦 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑎 = 𝑦) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}) |
20 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
21 | 9 | rabex 4740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ∈ V) |
23 | 4, 19, 20, 22 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑀‘𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑀‘𝑦) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦}) |
25 | 24 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀‘𝑦) ↔ 𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦})) |
26 | 14 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑡 → ((𝑤‘1) = 𝑦 ↔ (𝑡‘1) = 𝑦)) |
27 | 26 | elrab 3331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑦} ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦)) |
28 | 25, 27 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) |
29 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡‘1) = 𝑥 → ((𝑡‘1) = 𝑦 → 𝑥 = 𝑦)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡‘1) = 𝑦 → 𝑥 = 𝑦)) |
32 | 31 | adantld 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) |
33 | 28, 32 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → (𝑡 ∈ (𝑀‘𝑦) → 𝑥 = 𝑦)) |
34 | 33 | con3d 147 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦))) |
35 | 34 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑡‘1) = 𝑥 → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦)))) |
36 | 35 | adantld 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦)))) |
37 | 16, 36 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦)))) |
38 | 13, 37 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑥) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦)))) |
39 | 38 | com23 84 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (¬ 𝑥 = 𝑦 → (𝑡 ∈ (𝑀‘𝑥) → ¬ 𝑡 ∈ (𝑀‘𝑦)))) |
40 | 39 | imp31 447 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ¬ 𝑡 ∈ (𝑀‘𝑦)) |
41 | 40 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
42 | | disj 3969 |
. . . . . . 7
⊢ (((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
43 | 41, 42 | sylibr 223 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) |
44 | 43 | olcd 407 |
. . . . 5
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
45 | 44 | expcom 450 |
. . . 4
⊢ (¬
𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
46 | 2, 45 | pm2.61i 175 |
. . 3
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
47 | 46 | rgen2 2958 |
. 2
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) |
48 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) |
49 | 48 | disjor 4567 |
. 2
⊢
(Disj 𝑥
∈ 𝑉 (𝑀‘𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
50 | 47, 49 | mpbir 220 |
1
⊢
Disj 𝑥 ∈
𝑉 (𝑀‘𝑥) |