Step |
Hyp |
Ref |
Expression |
1 |
|
frgrhash2wsp.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fusgreg2wsp.m |
⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } ) |
3 |
|
orc |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) |
4 |
3
|
a1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) ) |
5 |
1 2
|
fusgreg2wsplem |
⊢ ( 𝑦 ∈ 𝑉 → ( 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) ) ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ) → ( 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) ) ) |
8 |
1 2
|
fusgreg2wsplem |
⊢ ( 𝑥 ∈ 𝑉 → ( 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ↔ ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑥 ) ) ) |
9 |
|
eqtr2 |
⊢ ( ( ( 𝑡 ‘ 1 ) = 𝑥 ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) |
10 |
9
|
expcom |
⊢ ( ( 𝑡 ‘ 1 ) = 𝑦 → ( ( 𝑡 ‘ 1 ) = 𝑥 → 𝑥 = 𝑦 ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → ( ( 𝑡 ‘ 1 ) = 𝑥 → 𝑥 = 𝑦 ) ) |
12 |
11
|
com12 |
⊢ ( ( 𝑡 ‘ 1 ) = 𝑥 → ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑥 ) → ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) ) |
14 |
8 13
|
syl6bi |
⊢ ( 𝑥 ∈ 𝑉 → ( 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) → ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) ) ) |
15 |
14
|
adantr |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) → ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) ) ) |
16 |
15
|
imp |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ) → ( ( 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑡 ‘ 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) ) |
17 |
7 16
|
sylbid |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ) → ( 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) |
18 |
17
|
con3d |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ) → ( ¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ) ) |
19 |
18
|
impancom |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) → ¬ 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ) ) |
20 |
19
|
ralrimiv |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ¬ 𝑥 = 𝑦 ) → ∀ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ¬ 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ) |
21 |
|
disj |
⊢ ( ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ↔ ∀ 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) ¬ 𝑡 ∈ ( 𝑀 ‘ 𝑦 ) ) |
22 |
20 21
|
sylibr |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) |
23 |
22
|
olcd |
⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) |
24 |
23
|
expcom |
⊢ ( ¬ 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) ) |
25 |
4 24
|
pm2.61i |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) |
26 |
25
|
rgen2 |
⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) |
27 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) ) |
28 |
27
|
disjor |
⊢ ( Disj 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 = 𝑦 ∨ ( ( 𝑀 ‘ 𝑥 ) ∩ ( 𝑀 ‘ 𝑦 ) ) = ∅ ) ) |
29 |
26 28
|
mpbir |
⊢ Disj 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) |