Step | Hyp | Ref
| Expression |
1 | | reclempr.1 |
. . . . . . 7
โข ๐ต = {๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด)} |
2 | 1 | reclem2pr 11039 |
. . . . . 6
โข (๐ด โ P โ
๐ต โ
P) |
3 | | df-mp 10975 |
. . . . . . 7
โข
ยทP = (๐ฆ โ P, ๐ค โ P โฆ {๐ข โฃ โ๐ โ ๐ฆ โ๐ โ ๐ค ๐ข = (๐ ยทQ ๐)}) |
4 | | mulclnq 10938 |
. . . . . . 7
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) โ Q) |
5 | 3, 4 | genpelv 10991 |
. . . . . 6
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ค โ (๐ด
ยทP ๐ต) โ โ๐ง โ ๐ด โ๐ฅ โ ๐ต ๐ค = (๐ง ยทQ ๐ฅ))) |
6 | 2, 5 | mpdan 686 |
. . . . 5
โข (๐ด โ P โ
(๐ค โ (๐ด
ยทP ๐ต) โ โ๐ง โ ๐ด โ๐ฅ โ ๐ต ๐ค = (๐ง ยทQ ๐ฅ))) |
7 | 1 | eqabri 2878 |
. . . . . . . . 9
โข (๐ฅ โ ๐ต โ โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด)) |
8 | | ltrelnq 10917 |
. . . . . . . . . . . . . . 15
โข
<Q โ (Q ร
Q) |
9 | 8 | brel 5739 |
. . . . . . . . . . . . . 14
โข (๐ฅ <Q
๐ฆ โ (๐ฅ โ Q โง
๐ฆ โ
Q)) |
10 | 9 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ฅ <Q
๐ฆ โ ๐ฆ โ Q) |
11 | | elprnq 10982 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ P โง
๐ง โ ๐ด) โ ๐ง โ Q) |
12 | | ltmnq 10963 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง โ Q โ
(๐ฅ
<Q ๐ฆ โ (๐ง ยทQ ๐ฅ) <Q
(๐ง
ยทQ ๐ฆ))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ <Q ๐ฆ โ (๐ง ยทQ ๐ฅ) <Q
(๐ง
ยทQ ๐ฆ))) |
14 | 13 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ <Q ๐ฆ โ (๐ง ยทQ ๐ฅ) <Q
(๐ง
ยทQ ๐ฆ))) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ (๐ฅ <Q
๐ฆ โ (๐ง
ยทQ ๐ฅ) <Q (๐ง
ยทQ ๐ฆ))) |
16 | | recclnq 10957 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ Q โ
(*Qโ๐ฆ) โ Q) |
17 | | prub 10985 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ P โง
๐ง โ ๐ด) โง
(*Qโ๐ฆ) โ Q) โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ ๐ง <Q
(*Qโ๐ฆ))) |
18 | 16, 17 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ ๐ง <Q
(*Qโ๐ฆ))) |
19 | | ltmnq 10963 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ Q โ
(๐ง
<Q (*Qโ๐ฆ) โ (๐ฆ ยทQ ๐ง) <Q
(๐ฆ
ยทQ (*Qโ๐ฆ)))) |
20 | | mulcomnq 10944 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ โ Q โ
(๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
22 | | recidnq 10956 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ โ Q โ
(๐ฆ
ยทQ (*Qโ๐ฆ)) =
1Q) |
23 | 21, 22 | breq12d 5160 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ Q โ
((๐ฆ
ยทQ ๐ง) <Q (๐ฆ
ยทQ (*Qโ๐ฆ)) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
24 | 19, 23 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ Q โ
(๐ง
<Q (*Qโ๐ฆ) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
25 | 24 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ (๐ง <Q
(*Qโ๐ฆ) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
26 | 18, 25 | sylibd 238 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
27 | 15, 26 | anim12d 610 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ ((๐ฅ <Q
๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด) โ ((๐ง ยทQ ๐ฅ) <Q
(๐ง
ยทQ ๐ฆ) โง (๐ง ยทQ ๐ฆ) <Q
1Q))) |
28 | | ltsonq 10960 |
. . . . . . . . . . . . . . . 16
โข
<Q Or Q |
29 | 28, 8 | sotri 6125 |
. . . . . . . . . . . . . . 15
โข (((๐ง
ยทQ ๐ฅ) <Q (๐ง
ยทQ ๐ฆ) โง (๐ง ยทQ ๐ฆ) <Q
1Q) โ (๐ง ยทQ ๐ฅ) <Q
1Q) |
30 | 27, 29 | syl6 35 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
๐ง โ ๐ด) โง ๐ฆ โ Q) โ ((๐ฅ <Q
๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด) โ (๐ง ยทQ ๐ฅ) <Q
1Q)) |
31 | 30 | exp4b 432 |
. . . . . . . . . . . . 13
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฆ โ Q โ (๐ฅ <Q
๐ฆ โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ (๐ง ยทQ ๐ฅ) <Q
1Q)))) |
32 | 10, 31 | syl5 34 |
. . . . . . . . . . . 12
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ <Q ๐ฆ โ (๐ฅ <Q ๐ฆ โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ (๐ง ยทQ ๐ฅ) <Q
1Q)))) |
33 | 32 | pm2.43d 53 |
. . . . . . . . . . 11
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ <Q ๐ฆ โ (ยฌ
(*Qโ๐ฆ) โ ๐ด โ (๐ง ยทQ ๐ฅ) <Q
1Q))) |
34 | 33 | impd 412 |
. . . . . . . . . 10
โข ((๐ด โ P โง
๐ง โ ๐ด) โ ((๐ฅ <Q ๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด) โ (๐ง ยทQ ๐ฅ) <Q
1Q)) |
35 | 34 | exlimdv 1937 |
. . . . . . . . 9
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ
(*Qโ๐ฆ) โ ๐ด) โ (๐ง ยทQ ๐ฅ) <Q
1Q)) |
36 | 7, 35 | biimtrid 241 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ โ ๐ต โ (๐ง ยทQ ๐ฅ) <Q
1Q)) |
37 | | breq1 5150 |
. . . . . . . . 9
โข (๐ค = (๐ง ยทQ ๐ฅ) โ (๐ค <Q
1Q โ (๐ง ยทQ ๐ฅ) <Q
1Q)) |
38 | 37 | biimprcd 249 |
. . . . . . . 8
โข ((๐ง
ยทQ ๐ฅ) <Q
1Q โ (๐ค = (๐ง ยทQ ๐ฅ) โ ๐ค <Q
1Q)) |
39 | 36, 38 | syl6 35 |
. . . . . . 7
โข ((๐ด โ P โง
๐ง โ ๐ด) โ (๐ฅ โ ๐ต โ (๐ค = (๐ง ยทQ ๐ฅ) โ ๐ค <Q
1Q))) |
40 | 39 | expimpd 455 |
. . . . . 6
โข (๐ด โ P โ
((๐ง โ ๐ด โง ๐ฅ โ ๐ต) โ (๐ค = (๐ง ยทQ ๐ฅ) โ ๐ค <Q
1Q))) |
41 | 40 | rexlimdvv 3211 |
. . . . 5
โข (๐ด โ P โ
(โ๐ง โ ๐ด โ๐ฅ โ ๐ต ๐ค = (๐ง ยทQ ๐ฅ) โ ๐ค <Q
1Q)) |
42 | 6, 41 | sylbid 239 |
. . . 4
โข (๐ด โ P โ
(๐ค โ (๐ด
ยทP ๐ต) โ ๐ค <Q
1Q)) |
43 | | df-1p 10973 |
. . . . 5
โข
1P = {๐ค โฃ ๐ค <Q
1Q} |
44 | 43 | eqabri 2878 |
. . . 4
โข (๐ค โ
1P โ ๐ค <Q
1Q) |
45 | 42, 44 | syl6ibr 252 |
. . 3
โข (๐ด โ P โ
(๐ค โ (๐ด
ยทP ๐ต) โ ๐ค โ
1P)) |
46 | 45 | ssrdv 3987 |
. 2
โข (๐ด โ P โ
(๐ด
ยทP ๐ต) โ
1P) |
47 | 1 | reclem3pr 11040 |
. 2
โข (๐ด โ P โ
1P โ (๐ด ยทP ๐ต)) |
48 | 46, 47 | eqssd 3998 |
1
โข (๐ด โ P โ
(๐ด
ยทP ๐ต) =
1P) |