Metamath Proof Explorer


Theorem 2wspmdisj

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) (Proof shortened by AV, 10-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v 𝑉 = ( Vtx ‘ 𝐺 )
fusgreg2wsp.m 𝑀 = ( 𝑎𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
Assertion 2wspmdisj Disj 𝑥𝑉 ( 𝑀𝑥 )

Proof

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 𝑥𝑉 ( 𝑀𝑥 )