Step | Hyp | Ref
| Expression |
1 | | df-imp 7470 |
. . . 4
โข
ยทP = (๐ค โ P, ๐ฃ โ P โฆ โจ{๐ฅ โ Q โฃ
โ๐ฆ โ
Q โ๐ง
โ Q (๐ฆ
โ (1st โ๐ค) โง ๐ง โ (1st โ๐ฃ) โง ๐ฅ = (๐ฆ ยทQ ๐ง))}, {๐ฅ โ Q โฃ โ๐ฆ โ Q
โ๐ง โ
Q (๐ฆ โ
(2nd โ๐ค)
โง ๐ง โ
(2nd โ๐ฃ)
โง ๐ฅ = (๐ฆ
ยทQ ๐ง))}โฉ) |
2 | 1 | genpelxp 7512 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) โ (๐ซ Q ร
๐ซ Q)) |
3 | | mulclnq 7377 |
. . . 4
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) โ Q) |
4 | 1, 3 | genpml 7518 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q ๐ โ
(1st โ(๐ด
ยทP ๐ต))) |
5 | 1, 3 | genpmu 7519 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q ๐ โ
(2nd โ(๐ด
ยทP ๐ต))) |
6 | 2, 4, 5 | jca32 310 |
. 2
โข ((๐ด โ P โง
๐ต โ P)
โ ((๐ด
ยทP ๐ต) โ (๐ซ Q ร
๐ซ Q) โง (โ๐ โ Q ๐ โ (1st โ(๐ด
ยทP ๐ต)) โง โ๐ โ Q ๐ โ (2nd โ(๐ด
ยทP ๐ต))))) |
7 | | ltmnqg 7402 |
. . . . 5
โข ((๐ฅ โ Q โง
๐ฆ โ Q
โง ๐ง โ
Q) โ (๐ฅ
<Q ๐ฆ โ (๐ง ยทQ ๐ฅ) <Q
(๐ง
ยทQ ๐ฆ))) |
8 | | mulcomnqg 7384 |
. . . . 5
โข ((๐ฅ โ Q โง
๐ฆ โ Q)
โ (๐ฅ
ยทQ ๐ฆ) = (๐ฆ ยทQ ๐ฅ)) |
9 | | mulnqprl 7569 |
. . . . 5
โข ((((๐ด โ P โง
๐ข โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ก โ (1st
โ๐ต))) โง ๐ฅ โ Q) โ
(๐ฅ
<Q (๐ข ยทQ ๐ก) โ ๐ฅ โ (1st โ(๐ด
ยทP ๐ต)))) |
10 | 1, 3, 7, 8, 9 | genprndl 7522 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q (๐ โ
(1st โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (1st โ(๐ด
ยทP ๐ต))))) |
11 | | mulnqpru 7570 |
. . . . 5
โข ((((๐ด โ P โง
๐ข โ (2nd
โ๐ด)) โง (๐ต โ P โง
๐ก โ (2nd
โ๐ต))) โง ๐ฅ โ Q) โ
((๐ข
ยทQ ๐ก) <Q ๐ฅ โ ๐ฅ โ (2nd โ(๐ด
ยทP ๐ต)))) |
12 | 1, 3, 7, 8, 11 | genprndu 7523 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q (๐ โ
(2nd โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (2nd โ(๐ด
ยทP ๐ต))))) |
13 | 10, 12 | jca 306 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ (โ๐ โ
Q (๐ โ
(1st โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (1st โ(๐ด
ยทP ๐ต)))) โง โ๐ โ Q (๐ โ (2nd โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (2nd โ(๐ด
ยทP ๐ต)))))) |
14 | 1, 3, 7, 8 | genpdisj 7524 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q ยฌ (๐
โ (1st โ(๐ด ยทP ๐ต)) โง ๐ โ (2nd โ(๐ด
ยทP ๐ต)))) |
15 | | mullocpr 7572 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ โ๐ โ
Q โ๐
โ Q (๐
<Q ๐ โ (๐ โ (1st โ(๐ด
ยทP ๐ต)) โจ ๐ โ (2nd โ(๐ด
ยทP ๐ต))))) |
16 | 13, 14, 15 | 3jca 1177 |
. 2
โข ((๐ด โ P โง
๐ต โ P)
โ ((โ๐ โ
Q (๐ โ
(1st โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (1st โ(๐ด
ยทP ๐ต)))) โง โ๐ โ Q (๐ โ (2nd โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (2nd โ(๐ด
ยทP ๐ต))))) โง โ๐ โ Q ยฌ (๐ โ (1st
โ(๐ด
ยทP ๐ต)) โง ๐ โ (2nd โ(๐ด
ยทP ๐ต))) โง โ๐ โ Q โ๐ โ Q (๐ <Q
๐ โ (๐ โ (1st
โ(๐ด
ยทP ๐ต)) โจ ๐ โ (2nd โ(๐ด
ยทP ๐ต)))))) |
17 | | elnp1st2nd 7477 |
. 2
โข ((๐ด
ยทP ๐ต) โ P โ (((๐ด
ยทP ๐ต) โ (๐ซ Q ร
๐ซ Q) โง (โ๐ โ Q ๐ โ (1st โ(๐ด
ยทP ๐ต)) โง โ๐ โ Q ๐ โ (2nd โ(๐ด
ยทP ๐ต)))) โง ((โ๐ โ Q (๐ โ (1st โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (1st โ(๐ด
ยทP ๐ต)))) โง โ๐ โ Q (๐ โ (2nd โ(๐ด
ยทP ๐ต)) โ โ๐ โ Q (๐ <Q ๐ โง ๐ โ (2nd โ(๐ด
ยทP ๐ต))))) โง โ๐ โ Q ยฌ (๐ โ (1st
โ(๐ด
ยทP ๐ต)) โง ๐ โ (2nd โ(๐ด
ยทP ๐ต))) โง โ๐ โ Q โ๐ โ Q (๐ <Q
๐ โ (๐ โ (1st
โ(๐ด
ยทP ๐ต)) โจ ๐ โ (2nd โ(๐ด
ยทP ๐ต))))))) |
18 | 6, 16, 17 | sylanbrc 417 |
1
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) โ P) |