Step | Hyp | Ref
| Expression |
1 | | df-ltpq 10853 |
. . . 4
โข
<pQ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ)))} |
2 | | opabssxp 5729 |
. . . 4
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ)))} โ ((N ร
N) ร (N ร
N)) |
3 | 1, 2 | eqsstri 3983 |
. . 3
โข
<pQ โ ((N ร
N) ร (N ร
N)) |
4 | 3 | brel 5702 |
. 2
โข (๐ด <pQ
๐ต โ (๐ด โ (N ร
N) โง ๐ต
โ (N ร N))) |
5 | | ltrelnq 10869 |
. . . 4
โข
<Q โ (Q ร
Q) |
6 | 5 | brel 5702 |
. . 3
โข
(([Q]โ๐ด) <Q
([Q]โ๐ต)
โ (([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q)) |
7 | | elpqn 10868 |
. . . 4
โข
(([Q]โ๐ด) โ Q โ
([Q]โ๐ด)
โ (N ร N)) |
8 | | elpqn 10868 |
. . . 4
โข
(([Q]โ๐ต) โ Q โ
([Q]โ๐ต)
โ (N ร N)) |
9 | | nqerf 10873 |
. . . . . . 7
โข
[Q]:(N ร
N)โถQ |
10 | 9 | fdmi 6685 |
. . . . . 6
โข dom
[Q] = (N ร N) |
11 | | 0nelxp 5672 |
. . . . . 6
โข ยฌ
โ
โ (N ร N) |
12 | 10, 11 | ndmfvrcl 6883 |
. . . . 5
โข
(([Q]โ๐ด) โ (N ร
N) โ ๐ด
โ (N ร N)) |
13 | 10, 11 | ndmfvrcl 6883 |
. . . . 5
โข
(([Q]โ๐ต) โ (N ร
N) โ ๐ต
โ (N ร N)) |
14 | 12, 13 | anim12i 614 |
. . . 4
โข
((([Q]โ๐ด) โ (N ร
N) โง ([Q]โ๐ต) โ (N ร
N)) โ (๐ด
โ (N ร N) โง ๐ต โ (N ร
N))) |
15 | 7, 8, 14 | syl2an 597 |
. . 3
โข
((([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q) โ (๐ด โ (N ร
N) โง ๐ต
โ (N ร N))) |
16 | 6, 15 | syl 17 |
. 2
โข
(([Q]โ๐ด) <Q
([Q]โ๐ต)
โ (๐ด โ
(N ร N) โง ๐ต โ (N ร
N))) |
17 | | xp1st 7958 |
. . . . 5
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
18 | | xp2nd 7959 |
. . . . 5
โข (๐ต โ (N ร
N) โ (2nd โ๐ต) โ N) |
19 | | mulclpi 10836 |
. . . . 5
โข
(((1st โ๐ด) โ N โง
(2nd โ๐ต)
โ N) โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
20 | 17, 18, 19 | syl2an 597 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((1st
โ๐ด)
ยทN (2nd โ๐ต)) โ N) |
21 | | ltmpi 10847 |
. . . 4
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) <N
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))) โ (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) <N
(((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))))) |
22 | 20, 21 | syl 17 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) <N
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))) โ (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) <N
(((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))))) |
23 | | nqercl 10874 |
. . . 4
โข (๐ด โ (N ร
N) โ ([Q]โ๐ด) โ Q) |
24 | | nqercl 10874 |
. . . 4
โข (๐ต โ (N ร
N) โ ([Q]โ๐ต) โ Q) |
25 | | ordpinq 10886 |
. . . 4
โข
((([Q]โ๐ด) โ Q โง
([Q]โ๐ต)
โ Q) โ (([Q]โ๐ด) <Q
([Q]โ๐ต)
โ ((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) <N
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))))) |
26 | 23, 24, 25 | syl2an 597 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ
(([Q]โ๐ด) <Q
([Q]โ๐ต)
โ ((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) <N
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))))) |
27 | | 1st2nd2 7965 |
. . . . . 6
โข (๐ด โ (N ร
N) โ ๐ด =
โจ(1st โ๐ด), (2nd โ๐ด)โฉ) |
28 | | 1st2nd2 7965 |
. . . . . 6
โข (๐ต โ (N ร
N) โ ๐ต =
โจ(1st โ๐ต), (2nd โ๐ต)โฉ) |
29 | 27, 28 | breqan12d 5126 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด <pQ ๐ต โ โจ(1st
โ๐ด), (2nd
โ๐ด)โฉ
<pQ โจ(1st โ๐ต), (2nd โ๐ต)โฉ)) |
30 | | ordpipq 10885 |
. . . . 5
โข
(โจ(1st โ๐ด), (2nd โ๐ด)โฉ <pQ
โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด))) |
31 | 29, 30 | bitrdi 287 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด <pQ ๐ต โ ((1st
โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
32 | | xp1st 7958 |
. . . . . . 7
โข
(([Q]โ๐ด) โ (N ร
N) โ (1st โ([Q]โ๐ด)) โ
N) |
33 | 23, 7, 32 | 3syl 18 |
. . . . . 6
โข (๐ด โ (N ร
N) โ (1st โ([Q]โ๐ด)) โ
N) |
34 | | xp2nd 7959 |
. . . . . . 7
โข
(([Q]โ๐ต) โ (N ร
N) โ (2nd โ([Q]โ๐ต)) โ
N) |
35 | 24, 8, 34 | 3syl 18 |
. . . . . 6
โข (๐ต โ (N ร
N) โ (2nd โ([Q]โ๐ต)) โ
N) |
36 | | mulclpi 10836 |
. . . . . 6
โข
(((1st โ([Q]โ๐ด)) โ N โง
(2nd โ([Q]โ๐ต)) โ N) โ
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) โ N) |
37 | 33, 35, 36 | syl2an 597 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) โ N) |
38 | | ltmpi 10847 |
. . . . 5
โข
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) โ N โ
(((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) <N
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))))) |
39 | 37, 38 | syl 17 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (((1st
โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) <N
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))))) |
40 | | mulcompi 10839 |
. . . . . 6
โข
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) = (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) |
41 | 40 | a1i 11 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) = (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))))) |
42 | | nqerrel 10875 |
. . . . . . . . 9
โข (๐ด โ (N ร
N) โ ๐ด
~Q ([Q]โ๐ด)) |
43 | 23, 7 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ (N ร
N) โ ([Q]โ๐ด) โ (N ร
N)) |
44 | | enqbreq2 10863 |
. . . . . . . . . 10
โข ((๐ด โ (N ร
N) โง ([Q]โ๐ด) โ (N ร
N)) โ (๐ด
~Q ([Q]โ๐ด) โ ((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด))) = ((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด)))) |
45 | 43, 44 | mpdan 686 |
. . . . . . . . 9
โข (๐ด โ (N ร
N) โ (๐ด
~Q ([Q]โ๐ด) โ ((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด))) = ((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด)))) |
46 | 42, 45 | mpbid 231 |
. . . . . . . 8
โข (๐ด โ (N ร
N) โ ((1st โ๐ด) ยทN
(2nd โ([Q]โ๐ด))) = ((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด))) |
47 | 46 | eqcomd 2743 |
. . . . . . 7
โข (๐ด โ (N ร
N) โ ((1st โ([Q]โ๐ด))
ยทN (2nd โ๐ด)) = ((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด)))) |
48 | | nqerrel 10875 |
. . . . . . . 8
โข (๐ต โ (N ร
N) โ ๐ต
~Q ([Q]โ๐ต)) |
49 | 24, 8 | syl 17 |
. . . . . . . . 9
โข (๐ต โ (N ร
N) โ ([Q]โ๐ต) โ (N ร
N)) |
50 | | enqbreq2 10863 |
. . . . . . . . 9
โข ((๐ต โ (N ร
N) โง ([Q]โ๐ต) โ (N ร
N)) โ (๐ต
~Q ([Q]โ๐ต) โ ((1st โ๐ต)
ยทN (2nd
โ([Q]โ๐ต))) = ((1st
โ([Q]โ๐ต)) ยทN
(2nd โ๐ต)))) |
51 | 49, 50 | mpdan 686 |
. . . . . . . 8
โข (๐ต โ (N ร
N) โ (๐ต
~Q ([Q]โ๐ต) โ ((1st โ๐ต)
ยทN (2nd
โ([Q]โ๐ต))) = ((1st
โ([Q]โ๐ต)) ยทN
(2nd โ๐ต)))) |
52 | 48, 51 | mpbid 231 |
. . . . . . 7
โข (๐ต โ (N ร
N) โ ((1st โ๐ต) ยทN
(2nd โ([Q]โ๐ต))) = ((1st
โ([Q]โ๐ต)) ยทN
(2nd โ๐ต))) |
53 | 47, 52 | oveqan12d 7381 |
. . . . . 6
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ต) ยทN
(2nd โ([Q]โ๐ต)))) = (((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด))) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ๐ต)))) |
54 | | mulcompi 10839 |
. . . . . . 7
โข
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))) = (((1st โ๐ต)
ยทN (2nd โ๐ด)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) |
55 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ๐ต) โ V |
56 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ๐ด) โ V |
57 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ([Q]โ๐ด)) โ V |
58 | | mulcompi 10839 |
. . . . . . . 8
โข (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ) |
59 | | mulasspi 10840 |
. . . . . . . 8
โข ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง)) |
60 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ([Q]โ๐ต)) โ V |
61 | 55, 56, 57, 58, 59, 60 | caov411 7591 |
. . . . . . 7
โข
(((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN ((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) = (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ต) ยทN
(2nd โ([Q]โ๐ต)))) |
62 | 54, 61 | eqtri 2765 |
. . . . . 6
โข
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))) = (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ต) ยทN
(2nd โ([Q]โ๐ต)))) |
63 | | mulcompi 10839 |
. . . . . . 7
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((1st
โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))) = (((1st
โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) |
64 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ([Q]โ๐ต)) โ V |
65 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ([Q]โ๐ด)) โ V |
66 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ๐ด) โ V |
67 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ๐ต) โ V |
68 | 64, 65, 66, 58, 59, 67 | caov411 7591 |
. . . . . . 7
โข
(((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) = (((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด))) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ๐ต))) |
69 | 63, 68 | eqtri 2765 |
. . . . . 6
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((1st
โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))) = (((1st โ๐ด)
ยทN (2nd
โ([Q]โ๐ด))) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ๐ต))) |
70 | 53, 62, 69 | 3eqtr4g 2802 |
. . . . 5
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))) = (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด))))) |
71 | 41, 70 | breq12d 5123 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ ((((1st
โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ต))) <N
(((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต))) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ด))) โ (((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) <N
(((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))))) |
72 | 31, 39, 71 | 3bitrd 305 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด <pQ ๐ต โ (((1st
โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ด)) ยทN
(2nd โ([Q]โ๐ต)))) <N
(((1st โ๐ด)
ยทN (2nd โ๐ต)) ยทN
((1st โ([Q]โ๐ต)) ยทN
(2nd โ([Q]โ๐ด)))))) |
73 | 22, 26, 72 | 3bitr4rd 312 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด <pQ ๐ต โ
([Q]โ๐ด)
<Q ([Q]โ๐ต))) |
74 | 4, 16, 73 | pm5.21nii 380 |
1
โข (๐ด <pQ
๐ต โ
([Q]โ๐ด)
<Q ([Q]โ๐ต)) |