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