Step | Hyp | Ref
| Expression |
1 | | wksonproplem.v |
. . . . . 6
⢠ð = (Vtxâðº) |
2 | 1 | fvexi 6905 |
. . . . 5
⢠ð â V |
3 | | wksonproplem.d |
. . . . . 6
⢠ð = (ð â V ⊠(ð â (Vtxâð), ð â (Vtxâð) ⊠{âšð, ð⩠⣠(ð(ð(ðâð)ð)ð â§ ð(ðâð)ð)})) |
4 | | simp1 1134 |
. . . . . . 7
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â ðº â V) |
5 | | simp2 1135 |
. . . . . . . 8
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â ðŽ â ð) |
6 | 5, 1 | eleqtrdi 2838 |
. . . . . . 7
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â ðŽ â (Vtxâðº)) |
7 | | simp3 1136 |
. . . . . . . 8
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â ðµ â ð) |
8 | 7, 1 | eleqtrdi 2838 |
. . . . . . 7
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â ðµ â (Vtxâðº)) |
9 | 4, 6, 8, 3 | mptmpoopabovd 8079 |
. . . . . 6
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â (ðŽ(ðâðº)ðµ) = {âšð, ð⩠⣠(ð(ðŽ(ðâðº)ðµ)ð â§ ð(ðâðº)ð)}) |
10 | | fveq2 6891 |
. . . . . . 7
⢠(ð = ðº â (Vtxâð) = (Vtxâðº)) |
11 | 10, 1 | eqtr4di 2785 |
. . . . . 6
⢠(ð = ðº â (Vtxâð) = ð) |
12 | | fveq2 6891 |
. . . . . . . . 9
⢠(ð = ðº â (ðâð) = (ðâðº)) |
13 | 12 | oveqd 7431 |
. . . . . . . 8
⢠(ð = ðº â (ð(ðâð)ð) = (ð(ðâðº)ð)) |
14 | 13 | breqd 5153 |
. . . . . . 7
⢠(ð = ðº â (ð(ð(ðâð)ð)ð â ð(ð(ðâðº)ð)ð)) |
15 | | fveq2 6891 |
. . . . . . . 8
⢠(ð = ðº â (ðâð) = (ðâðº)) |
16 | 15 | breqd 5153 |
. . . . . . 7
⢠(ð = ðº â (ð(ðâð)ð â ð(ðâðº)ð)) |
17 | 14, 16 | anbi12d 630 |
. . . . . 6
⢠(ð = ðº â ((ð(ð(ðâð)ð)ð â§ ð(ðâð)ð) â (ð(ð(ðâðº)ð)ð â§ ð(ðâðº)ð))) |
18 | 3, 9, 11, 11, 17 | bropfvvvv 8089 |
. . . . 5
⢠((ð â V â§ ð â V) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ðº â V â§ (ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)))) |
19 | 2, 2, 18 | mp2an 691 |
. . . 4
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â (ðº â V â§ (ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V))) |
20 | | 3anass 1093 |
. . . . . 6
⢠((ðº â V â§ ðŽ â ð â§ ðµ â ð) â (ðº â V â§ (ðŽ â ð â§ ðµ â ð))) |
21 | 20 | anbi1i 623 |
. . . . 5
⢠(((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â ((ðº â V â§ (ðŽ â ð â§ ðµ â ð)) â§ (ð¹ â V â§ ð â V))) |
22 | | df-3an 1087 |
. . . . 5
⢠((ðº â V â§ (ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â ((ðº â V â§ (ðŽ â ð â§ ðµ â ð)) â§ (ð¹ â V â§ ð â V))) |
23 | 21, 22 | bitr4i 278 |
. . . 4
⢠(((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â (ðº â V â§ (ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V))) |
24 | 19, 23 | sylibr 233 |
. . 3
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â ((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V))) |
25 | | wksonproplem.b |
. . . . 5
⢠(((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |
26 | 25 | biimpd 228 |
. . . 4
⢠(((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â (ð¹(ðŽ(ðâðº)ðµ)ð â (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |
27 | 26 | imdistani 568 |
. . 3
⢠((((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â§ ð¹(ðŽ(ðâðº)ðµ)ð) â (((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â§ (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |
28 | 24, 27 | mpancom 687 |
. 2
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â (((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â§ (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |
29 | | df-3an 1087 |
. 2
⢠(((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V) â§ (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð)) â (((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V)) â§ (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |
30 | 28, 29 | sylibr 233 |
1
⢠(ð¹(ðŽ(ðâðº)ðµ)ð â ((ðº â V â§ ðŽ â ð â§ ðµ â ð) â§ (ð¹ â V â§ ð â V) â§ (ð¹(ðŽ(ðâðº)ðµ)ð â§ ð¹(ðâðº)ð))) |