Step | Hyp | Ref
| Expression |
1 | | orc 866 |
. . . . 5
⢠(ð¥ = ðŠ â (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
)) |
2 | 1 | a1d 25 |
. . . 4
⢠(ð¥ = ðŠ â ((ð¥ â ð ⧠ðŠ â ð) â (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
))) |
3 | | frgrhash2wsp.v |
. . . . . . . . . . . . . 14
⢠ð = (Vtxâðº) |
4 | | fusgreg2wsp.m |
. . . . . . . . . . . . . 14
⢠ð = (ð â ð ⊠{ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð}) |
5 | 3, 4 | fusgreg2wsplem 29319 |
. . . . . . . . . . . . 13
⢠(ðŠ â ð â (ð¡ â (ðâðŠ) â (ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ))) |
6 | 5 | adantl 483 |
. . . . . . . . . . . 12
⢠((ð¥ â ð ⧠ðŠ â ð) â (ð¡ â (ðâðŠ) â (ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ))) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð¡ â (ðâð¥)) â (ð¡ â (ðâðŠ) â (ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ))) |
8 | 3, 4 | fusgreg2wsplem 29319 |
. . . . . . . . . . . . . 14
⢠(ð¥ â ð â (ð¡ â (ðâð¥) â (ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ð¥))) |
9 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . 18
⢠(((ð¡â1) = ð¥ ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ) |
10 | 9 | expcom 415 |
. . . . . . . . . . . . . . . . 17
⢠((ð¡â1) = ðŠ â ((ð¡â1) = ð¥ â ð¥ = ðŠ)) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . . . . 16
⢠((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ((ð¡â1) = ð¥ â ð¥ = ðŠ)) |
12 | 11 | com12 32 |
. . . . . . . . . . . . . . 15
⢠((ð¡â1) = ð¥ â ((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ)) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . 14
⢠((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ð¥) â ((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ)) |
14 | 8, 13 | syl6bi 253 |
. . . . . . . . . . . . 13
⢠(ð¥ â ð â (ð¡ â (ðâð¥) â ((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ))) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
⢠((ð¥ â ð ⧠ðŠ â ð) â (ð¡ â (ðâð¥) â ((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ))) |
16 | 15 | imp 408 |
. . . . . . . . . . 11
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð¡ â (ðâð¥)) â ((ð¡ â (2 WSPathsN ðº) ⧠(ð¡â1) = ðŠ) â ð¥ = ðŠ)) |
17 | 7, 16 | sylbid 239 |
. . . . . . . . . 10
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð¡ â (ðâð¥)) â (ð¡ â (ðâðŠ) â ð¥ = ðŠ)) |
18 | 17 | con3d 152 |
. . . . . . . . 9
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð¡ â (ðâð¥)) â (¬ ð¥ = ðŠ â ¬ ð¡ â (ðâðŠ))) |
19 | 18 | impancom 453 |
. . . . . . . 8
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠¬ ð¥ = ðŠ) â (ð¡ â (ðâð¥) â ¬ ð¡ â (ðâðŠ))) |
20 | 19 | ralrimiv 3143 |
. . . . . . 7
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠¬ ð¥ = ðŠ) â âð¡ â (ðâð¥) ¬ ð¡ â (ðâðŠ)) |
21 | | disj 4412 |
. . . . . . 7
⢠(((ðâð¥) â© (ðâðŠ)) = â
â âð¡ â (ðâð¥) ¬ ð¡ â (ðâðŠ)) |
22 | 20, 21 | sylibr 233 |
. . . . . 6
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠¬ ð¥ = ðŠ) â ((ðâð¥) â© (ðâðŠ)) = â
) |
23 | 22 | olcd 873 |
. . . . 5
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠¬ ð¥ = ðŠ) â (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
)) |
24 | 23 | expcom 415 |
. . . 4
⢠(¬
ð¥ = ðŠ â ((ð¥ â ð ⧠ðŠ â ð) â (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
))) |
25 | 2, 24 | pm2.61i 182 |
. . 3
⢠((ð¥ â ð ⧠ðŠ â ð) â (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
)) |
26 | 25 | rgen2 3195 |
. 2
â¢
âð¥ â
ð âðŠ â ð (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
) |
27 | | fveq2 6847 |
. . 3
⢠(ð¥ = ðŠ â (ðâð¥) = (ðâðŠ)) |
28 | 27 | disjor 5090 |
. 2
â¢
(Disj ð¥
â ð (ðâð¥) â âð¥ â ð âðŠ â ð (ð¥ = ðŠ âš ((ðâð¥) â© (ðâðŠ)) = â
)) |
29 | 26, 28 | mpbir 230 |
1
â¢
Disj ð¥ â
ð (ðâð¥) |