Step | Hyp | Ref
| Expression |
1 | | iswwlksnon.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wwlksnon 26738 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})) |
3 | 2 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})) |
4 | | eqeq2 2633 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑤‘0) = 𝑎 ↔ (𝑤‘0) = 𝐴)) |
5 | | eqeq2 2633 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑤‘𝑁) = 𝑏 ↔ (𝑤‘𝑁) = 𝐵)) |
6 | 4, 5 | bi2anan9 917 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏) ↔ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵))) |
7 | 6 | rabbidv 3189 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |
8 | 7 | adantl 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |
9 | | simprl 794 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
10 | | simprr 796 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
11 | | ovex 6678 |
. . . . . 6
⊢ (𝑁 WWalksN 𝐺) ∈ V |
12 | 11 | rabex 4813 |
. . . . 5
⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} ∈ V |
13 | 12 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} ∈ V) |
14 | 3, 8, 9, 10, 13 | ovmpt2d 6788 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |
15 | 14 | ex 450 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})) |
16 | | 0ov 6682 |
. . . 4
⊢ (𝐴∅𝐵) = ∅ |
17 | | df-wwlksnon 26724 |
. . . . . 6
⊢
WWalksNOn = (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ (𝑎 ∈
(Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})) |
18 | 17 | mpt2ndm0 6875 |
. . . . 5
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑁
WWalksNOn 𝐺) =
∅) |
19 | 18 | oveqd 6667 |
. . . 4
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = (𝐴∅𝐵)) |
20 | | df-wwlksn 26723 |
. . . . . . 7
⊢ WWalksN
= (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ {𝑤 ∈
(WWalks‘𝑔) ∣
(#‘𝑤) = (𝑛 + 1)}) |
21 | 20 | mpt2ndm0 6875 |
. . . . . 6
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑁 WWalksN
𝐺) =
∅) |
22 | 21 | rabeqdv 3194 |
. . . . 5
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → {𝑤 ∈
(𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = {𝑤 ∈ ∅ ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |
23 | | rab0 3955 |
. . . . 5
⊢ {𝑤 ∈ ∅ ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅ |
24 | 22, 23 | syl6eq 2672 |
. . . 4
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → {𝑤 ∈
(𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)} = ∅) |
25 | 16, 19, 24 | 3eqtr4a 2682 |
. . 3
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |
26 | 25 | a1d 25 |
. 2
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → ((𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)})) |
27 | 15, 26 | pm2.61i 176 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) |