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 biimtrdi ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑡 ∈ ( 𝑀 ‘ 𝑥 ) → ( ( 𝑡 ∈ ( 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 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 )