Step | Hyp | Ref
| Expression |
1 | | mulnqprlemru 7572 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ (2nd โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โ
(2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) |
2 | | ltsonq 7396 |
. . . . . . . . 9
โข
<Q Or Q |
3 | | mulclnq 7374 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
ยทQ ๐ต) โ Q) |
4 | | sonr 4317 |
. . . . . . . . 9
โข ((
<Q Or Q โง (๐ด ยทQ ๐ต) โ Q) โ
ยฌ (๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต)) |
5 | 2, 3, 4 | sylancr 414 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q)
โ ยฌ (๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต)) |
6 | | ltrelnq 7363 |
. . . . . . . . . . . 12
โข
<Q โ (Q ร
Q) |
7 | 6 | brel 4678 |
. . . . . . . . . . 11
โข ((๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต) โ ((๐ด ยทQ ๐ต) โ Q โง
(๐ด
ยทQ ๐ต) โ Q)) |
8 | 7 | simpld 112 |
. . . . . . . . . 10
โข ((๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต) โ (๐ด ยทQ ๐ต) โ
Q) |
9 | | elex 2748 |
. . . . . . . . . 10
โข ((๐ด
ยทQ ๐ต) โ Q โ (๐ด
ยทQ ๐ต) โ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
โข ((๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต) โ (๐ด ยทQ ๐ต) โ V) |
11 | | breq2 4007 |
. . . . . . . . 9
โข (๐ข = (๐ด ยทQ ๐ต) โ ((๐ด ยทQ ๐ต) <Q
๐ข โ (๐ด ยทQ ๐ต) <Q
(๐ด
ยทQ ๐ต))) |
12 | 10, 11 | elab3 2889 |
. . . . . . . 8
โข ((๐ด
ยทQ ๐ต) โ {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข} โ (๐ด
ยทQ ๐ต) <Q (๐ด
ยทQ ๐ต)) |
13 | 5, 12 | sylnibr 677 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q)
โ ยฌ (๐ด
ยทQ ๐ต) โ {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}) |
14 | | ltnqex 7547 |
. . . . . . . . 9
โข {๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)} โ V |
15 | | gtnqex 7548 |
. . . . . . . . 9
โข {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข} โ
V |
16 | 14, 15 | op2nd 6147 |
. . . . . . . 8
โข
(2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข} |
17 | 16 | eleq2i 2244 |
. . . . . . 7
โข ((๐ด
ยทQ ๐ต) โ (2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ (๐ด
ยทQ ๐ต) โ {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}) |
18 | 13, 17 | sylnibr 677 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ ยฌ (๐ด
ยทQ ๐ต) โ (2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) |
19 | 1, 18 | ssneldd 3158 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ยฌ (๐ด
ยทQ ๐ต) โ (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
20 | 19 | adantr 276 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q)
โง ๐ โ
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) โ ยฌ
(๐ด
ยทQ ๐ต) โ (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
21 | | nqprlu 7545 |
. . . . . . 7
โข (๐ด โ Q โ
โจ{๐ โฃ ๐ <Q
๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ โ
P) |
22 | | nqprlu 7545 |
. . . . . . 7
โข (๐ต โ Q โ
โจ{๐ โฃ ๐ <Q
๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ โ
P) |
23 | | mulclpr 7570 |
. . . . . . 7
โข
((โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ โ P
โง โจ{๐ โฃ
๐
<Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ โ P)
โ (โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ
P) |
24 | 21, 22, 23 | syl2an 289 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ (โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ
P) |
25 | | prop 7473 |
. . . . . 6
โข
((โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ P
โ โจ(1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)), (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))โฉ โ
P) |
26 | 24, 25 | syl 14 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ โจ(1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)), (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))โฉ โ
P) |
27 | | vex 2740 |
. . . . . . 7
โข ๐ โ V |
28 | | breq1 4006 |
. . . . . . 7
โข (๐ = ๐ โ (๐ <Q (๐ด
ยทQ ๐ต) โ ๐ <Q (๐ด
ยทQ ๐ต))) |
29 | 14, 15 | op1st 6146 |
. . . . . . 7
โข
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = {๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)} |
30 | 27, 28, 29 | elab2 2885 |
. . . . . 6
โข (๐ โ (1st
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ ๐ <Q
(๐ด
ยทQ ๐ต)) |
31 | 30 | biimpi 120 |
. . . . 5
โข (๐ โ (1st
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ ๐ <Q
(๐ด
ยทQ ๐ต)) |
32 | | prloc 7489 |
. . . . 5
โข
((โจ(1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)), (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))โฉ โ
P โง ๐
<Q (๐ด ยทQ ๐ต)) โ (๐ โ (1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โจ (๐ด
ยทQ ๐ต) โ (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)))) |
33 | 26, 31, 32 | syl2an 289 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q)
โง ๐ โ
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) โ (๐ โ (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โจ (๐ด
ยทQ ๐ต) โ (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)))) |
34 | 20, 33 | ecased 1349 |
. . 3
โข (((๐ด โ Q โง
๐ต โ Q)
โง ๐ โ
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) โ ๐ โ (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
35 | 34 | ex 115 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ โ
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ ๐ โ (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)))) |
36 | 35 | ssrdv 3161 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ
(1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |