Step | Hyp | Ref
| Expression |
1 | | df-wwlksnon 28606 |
. . 3
â¢
WWalksNOn = (ð â
â0, ð
â V ⊠(ð â
(Vtxâð), ð â (Vtxâð) ⊠{ð€ â (ð WWalksN ð) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)})) |
2 | 1 | a1i 11 |
. 2
⢠((ð â â0
⧠ðº â ð) â WWalksNOn = (ð â â0,
ð â V ⊠(ð â (Vtxâð), ð â (Vtxâð) ⊠{ð€ â (ð WWalksN ð) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}))) |
3 | | fveq2 6839 |
. . . . . 6
⢠(ð = ðº â (Vtxâð) = (Vtxâðº)) |
4 | | wwlksnon.v |
. . . . . 6
⢠ð = (Vtxâðº) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
⢠(ð = ðº â (Vtxâð) = ð) |
6 | 5 | adantl 482 |
. . . 4
⢠((ð = ð ⧠ð = ðº) â (Vtxâð) = ð) |
7 | | oveq12 7360 |
. . . . 5
⢠((ð = ð ⧠ð = ðº) â (ð WWalksN ð) = (ð WWalksN ðº)) |
8 | | fveqeq2 6848 |
. . . . . . 7
⢠(ð = ð â ((ð€âð) = ð â (ð€âð) = ð)) |
9 | 8 | anbi2d 629 |
. . . . . 6
⢠(ð = ð â (((ð€â0) = ð ⧠(ð€âð) = ð) â ((ð€â0) = ð ⧠(ð€âð) = ð))) |
10 | 9 | adantr 481 |
. . . . 5
⢠((ð = ð ⧠ð = ðº) â (((ð€â0) = ð ⧠(ð€âð) = ð) â ((ð€â0) = ð ⧠(ð€âð) = ð))) |
11 | 7, 10 | rabeqbidv 3422 |
. . . 4
⢠((ð = ð ⧠ð = ðº) â {ð€ â (ð WWalksN ð) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)} = {ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}) |
12 | 6, 6, 11 | mpoeq123dv 7426 |
. . 3
⢠((ð = ð ⧠ð = ðº) â (ð â (Vtxâð), ð â (Vtxâð) ⊠{ð€ â (ð WWalksN ð) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}) = (ð â ð, ð â ð ⊠{ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)})) |
13 | 12 | adantl 482 |
. 2
⢠(((ð â â0
⧠ðº â ð) ⧠(ð = ð ⧠ð = ðº)) â (ð â (Vtxâð), ð â (Vtxâð) ⊠{ð€ â (ð WWalksN ð) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}) = (ð â ð, ð â ð ⊠{ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)})) |
14 | | simpl 483 |
. 2
⢠((ð â â0
⧠ðº â ð) â ð â
â0) |
15 | | elex 3461 |
. . 3
⢠(ðº â ð â ðº â V) |
16 | 15 | adantl 482 |
. 2
⢠((ð â â0
⧠ðº â ð) â ðº â V) |
17 | 4 | fvexi 6853 |
. . . 4
⢠ð â V |
18 | 17, 17 | mpoex 8004 |
. . 3
⢠(ð â ð, ð â ð ⊠{ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}) â V |
19 | 18 | a1i 11 |
. 2
⢠((ð â â0
⧠ðº â ð) â (ð â ð, ð â ð ⊠{ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)}) â V) |
20 | 2, 13, 14, 16, 19 | ovmpod 7501 |
1
⢠((ð â â0
⧠ðº â ð) â (ð WWalksNOn ðº) = (ð â ð, ð â ð ⊠{ð€ â (ð WWalksN ðº) ⣠((ð€â0) = ð ⧠(ð€âð) = ð)})) |