Step | Hyp | Ref
| Expression |
1 | | iswwlksnon.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wspthsnon 41050 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑁 WSPathsNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤})) |
3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑁 WSPathsNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤})) |
4 | | oveq12 6558 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎(𝑁 WWalksNOn 𝐺)𝑏) = (𝐴(𝑁 WWalksNOn 𝐺)𝐵)) |
5 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎(SPathsOn‘𝐺)𝑏) = (𝐴(SPathsOn‘𝐺)𝐵)) |
6 | 5 | breqd 4594 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤 ↔ 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)) |
7 | 6 | exbidv 1837 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤 ↔ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)) |
8 | 4, 7 | rabeqbidv 3168 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤} = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |
9 | 8 | adantl 481 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤} = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |
10 | | simprl 790 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
11 | | simprr 792 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
12 | | ovex 6577 |
. . . . . 6
⊢ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∈ V |
13 | 12 | rabex 4740 |
. . . . 5
⊢ {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} ∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} ∈ V) |
15 | 3, 9, 10, 11, 14 | ovmpt2d 6686 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |
16 | 15 | ex 449 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤})) |
17 | | 0ov 6580 |
. . . 4
⊢ (𝐴∅𝐵) = ∅ |
18 | | df-wspthsnon 41037 |
. . . . . 6
⊢
WSPathsNOn = (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ (𝑎 ∈
(Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤})) |
19 | 18 | mpt2ndm0 6773 |
. . . . 5
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑁
WSPathsNOn 𝐺) =
∅) |
20 | 19 | oveqd 6566 |
. . . 4
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = (𝐴∅𝐵)) |
21 | | df-wwlksnon 41035 |
. . . . . . . . 9
⊢
WWalksNOn = (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ (𝑎 ∈
(Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})) |
22 | 21 | mpt2ndm0 6773 |
. . . . . . . 8
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑁
WWalksNOn 𝐺) =
∅) |
23 | 22 | oveqd 6566 |
. . . . . . 7
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = (𝐴∅𝐵)) |
24 | 23, 17 | syl6eq 2660 |
. . . . . 6
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅) |
25 | 24 | rabeqdv 3167 |
. . . . 5
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → {𝑤 ∈
(𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} = {𝑤 ∈ ∅ ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |
26 | | rab0 3909 |
. . . . 5
⊢ {𝑤 ∈ ∅ ∣
∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} = ∅ |
27 | 25, 26 | syl6eq 2660 |
. . . 4
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → {𝑤 ∈
(𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} = ∅) |
28 | 17, 20, 27 | 3eqtr4a 2670 |
. . 3
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |
29 | 28 | a1d 25 |
. 2
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → ((𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤})) |
30 | 16, 29 | pm2.61i 175 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) |