Metamath Proof Explorer

Theorem wspniunwspnon

Description: The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021) (Proof shortened by AV, 15-Mar-2022)

Ref Expression
Hypothesis wspniunwspnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wspniunwspnon ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WSPathsN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) )

Proof

Step Hyp Ref Expression
1 wspniunwspnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wspthsnonn0vne ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ≠ ∅ ) → 𝑥 ≠ 𝑦 )
3 2 ex ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ≠ ∅ → 𝑥 ≠ 𝑦 ) )
4 3 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ≠ ∅ → 𝑥 ≠ 𝑦 ) )
5 ne0i ⊢ ( 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) → ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ≠ ∅ )
6 4 5 impel ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) ∧ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) → 𝑥 ≠ 𝑦 )
7 6 necomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) ∧ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) → 𝑦 ≠ 𝑥 )
8 7 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) → 𝑦 ≠ 𝑥 ) )
9 8 pm4.71rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ( 𝑦 ≠ 𝑥 ∧ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) ) )
10 9 rexbidv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( ∃ 𝑦 ∈ 𝑉 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) ) )
11 rexdifsn ⊢ ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑉 ( 𝑦 ≠ 𝑥 ∧ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
12 10 11 bitr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( ∃ 𝑦 ∈ 𝑉 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
13 12 rexbidv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
14 1 wspthsnwspthsnon ⊢ ( 𝑤 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) )
15 vex ⊢ 𝑤 ∈ V
16 eleq1w ⊢ ( 𝑝 = 𝑤 → ( 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
17 16 rexbidv ⊢ ( 𝑝 = 𝑤 → ( ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
18 17 rexbidv ⊢ ( 𝑝 = 𝑤 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) ) )
19 15 18 elab ⊢ ( 𝑤 ∈ { 𝑝 ∣ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) } ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑤 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) )
20 13 14 19 3bitr4g ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑤 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ 𝑤 ∈ { 𝑝 ∣ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) } ) )
21 20 eqrdv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WSPathsN 𝐺 ) = { 𝑝 ∣ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) } )
22 dfiunv2 ⊢ ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) = { 𝑝 ∣ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) 𝑝 ∈ ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) }
23 21 22 eqtr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈 ) → ( 𝑁 WSPathsN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑥 ( 𝑁 WSPathsNOn 𝐺 ) 𝑦 ) )