Step | Hyp | Ref
| Expression |
1 | | wspthsnonn0vne 29715 |
. . . . . . . . . . . . 13
⢠((ð â â â§ (ð¥(ð WSPathsNOn ðº)ðŠ) â â
) â ð¥ â ðŠ) |
2 | 1 | ex 412 |
. . . . . . . . . . . 12
⢠(ð â â â ((ð¥(ð WSPathsNOn ðº)ðŠ) â â
â ð¥ â ðŠ)) |
3 | 2 | adantr 480 |
. . . . . . . . . . 11
⢠((ð â â â§ ðº â ð) â ((ð¥(ð WSPathsNOn ðº)ðŠ) â â
â ð¥ â ðŠ)) |
4 | | ne0i 4330 |
. . . . . . . . . . 11
⢠(ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â (ð¥(ð WSPathsNOn ðº)ðŠ) â â
) |
5 | 3, 4 | impel 505 |
. . . . . . . . . 10
⢠(((ð â â â§ ðº â ð) â§ ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)) â ð¥ â ðŠ) |
6 | 5 | necomd 2991 |
. . . . . . . . 9
⢠(((ð â â â§ ðº â ð) â§ ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)) â ðŠ â ð¥) |
7 | 6 | ex 412 |
. . . . . . . 8
⢠((ð â â â§ ðº â ð) â (ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â ðŠ â ð¥)) |
8 | 7 | pm4.71rd 562 |
. . . . . . 7
⢠((ð â â â§ ðº â ð) â (ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â (ðŠ â ð¥ â§ ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)))) |
9 | 8 | rexbidv 3173 |
. . . . . 6
⢠((ð â â â§ ðº â ð) â (âðŠ â ð ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â âðŠ â ð (ðŠ â ð¥ â§ ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)))) |
10 | | rexdifsn 4793 |
. . . . . 6
â¢
(âðŠ â
(ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â âðŠ â ð (ðŠ â ð¥ â§ ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
11 | 9, 10 | bitr4di 289 |
. . . . 5
⢠((ð â â â§ ðº â ð) â (âðŠ â ð ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â âðŠ â (ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
12 | 11 | rexbidv 3173 |
. . . 4
⢠((ð â â â§ ðº â ð) â (âð¥ â ð âðŠ â ð ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ) â âð¥ â ð âðŠ â (ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
13 | | wspniunwspnon.v |
. . . . 5
⢠ð = (Vtxâðº) |
14 | 13 | wspthsnwspthsnon 29714 |
. . . 4
⢠(ð€ â (ð WSPathsN ðº) â âð¥ â ð âðŠ â ð ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)) |
15 | | vex 3473 |
. . . . 5
⢠ð€ â V |
16 | | eleq1w 2811 |
. . . . . . 7
⢠(ð = ð€ â (ð â (ð¥(ð WSPathsNOn ðº)ðŠ) â ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
17 | 16 | rexbidv 3173 |
. . . . . 6
⢠(ð = ð€ â (âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ) â âðŠ â (ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
18 | 17 | rexbidv 3173 |
. . . . 5
⢠(ð = ð€ â (âð¥ â ð âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ) â âð¥ â ð âðŠ â (ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ))) |
19 | 15, 18 | elab 3665 |
. . . 4
⢠(ð€ â {ð ⣠âð¥ â ð âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ)} â âð¥ â ð âðŠ â (ð â {ð¥})ð€ â (ð¥(ð WSPathsNOn ðº)ðŠ)) |
20 | 12, 14, 19 | 3bitr4g 314 |
. . 3
⢠((ð â â â§ ðº â ð) â (ð€ â (ð WSPathsN ðº) â ð€ â {ð ⣠âð¥ â ð âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ)})) |
21 | 20 | eqrdv 2725 |
. 2
⢠((ð â â â§ ðº â ð) â (ð WSPathsN ðº) = {ð ⣠âð¥ â ð âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ)}) |
22 | | dfiunv2 5032 |
. 2
⢠⪠ð¥ â ð ⪠ðŠ â (ð â {ð¥})(ð¥(ð WSPathsNOn ðº)ðŠ) = {ð ⣠âð¥ â ð âðŠ â (ð â {ð¥})ð â (ð¥(ð WSPathsNOn ðº)ðŠ)} |
23 | 21, 22 | eqtr4di 2785 |
1
⢠((ð â â â§ ðº â ð) â (ð WSPathsN ðº) = âª
ð¥ â ð ⪠ðŠ â (ð â {ð¥})(ð¥(ð WSPathsNOn ðº)ðŠ)) |