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 𝐺 ) 𝑦 ) )