Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
โข ๐ต = โจ{๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด))}, {๐ฅ โฃ โ๐ฆ(๐ฆ <Q ๐ฅ โง
(*Qโ๐ฆ) โ (1st โ๐ด))}โฉ |
2 | 1 | recexprlempr 7630 |
. . . . 5
โข (๐ด โ P โ
๐ต โ
P) |
3 | | df-imp 7467 |
. . . . . 6
โข
ยทP = (๐ฆ โ P, ๐ค โ P โฆ โจ{๐ข โ Q โฃ
โ๐ โ
Q โ๐
โ Q (๐
โ (1st โ๐ฆ) โง ๐ โ (1st โ๐ค) โง ๐ข = (๐ ยทQ ๐))}, {๐ข โ Q โฃ โ๐ โ Q
โ๐ โ
Q (๐ โ
(2nd โ๐ฆ)
โง ๐ โ
(2nd โ๐ค)
โง ๐ข = (๐
ยทQ ๐))}โฉ) |
4 | | mulclnq 7374 |
. . . . . 6
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) โ Q) |
5 | 3, 4 | genpelvl 7510 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ค โ
(1st โ(๐ด
ยทP ๐ต)) โ โ๐ง โ (1st โ๐ด)โ๐ โ (1st โ๐ต)๐ค = (๐ง ยทQ ๐))) |
6 | 2, 5 | mpdan 421 |
. . . 4
โข (๐ด โ P โ
(๐ค โ (1st
โ(๐ด
ยทP ๐ต)) โ โ๐ง โ (1st โ๐ด)โ๐ โ (1st โ๐ต)๐ค = (๐ง ยทQ ๐))) |
7 | 1 | recexprlemell 7620 |
. . . . . . . 8
โข (๐ โ (1st
โ๐ต) โ
โ๐ฆ(๐ <Q ๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด))) |
8 | | ltrelnq 7363 |
. . . . . . . . . . . . . 14
โข
<Q โ (Q ร
Q) |
9 | 8 | brel 4678 |
. . . . . . . . . . . . 13
โข (๐ <Q
๐ฆ โ (๐ โ Q โง
๐ฆ โ
Q)) |
10 | 9 | simprd 114 |
. . . . . . . . . . . 12
โข (๐ <Q
๐ฆ โ ๐ฆ โ Q) |
11 | | prop 7473 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
12 | | elprnql 7479 |
. . . . . . . . . . . . . . . . . 18
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ง โ (1st
โ๐ด)) โ ๐ง โ
Q) |
13 | 11, 12 | sylan 283 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ ๐ง โ
Q) |
14 | | ltmnqi 7401 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ <Q
๐ฆ โง ๐ง โ Q) โ (๐ง
ยทQ ๐) <Q (๐ง
ยทQ ๐ฆ)) |
15 | 14 | expcom 116 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ Q โ
(๐
<Q ๐ฆ โ (๐ง ยทQ ๐) <Q
(๐ง
ยทQ ๐ฆ))) |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ <Q
๐ฆ โ (๐ง
ยทQ ๐) <Q (๐ง
ยทQ ๐ฆ))) |
17 | 16 | adantr 276 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
(๐
<Q ๐ฆ โ (๐ง ยทQ ๐) <Q
(๐ง
ยทQ ๐ฆ))) |
18 | | prltlu 7485 |
. . . . . . . . . . . . . . . . . . 19
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ง โ (1st
โ๐ด) โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ ๐ง <Q
(*Qโ๐ฆ)) |
19 | 11, 18 | syl3an1 1271 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด) โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ ๐ง <Q
(*Qโ๐ฆ)) |
20 | 19 | 3expia 1205 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ ๐ง <Q
(*Qโ๐ฆ))) |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ ๐ง <Q
(*Qโ๐ฆ))) |
22 | | ltmnqi 7401 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ง <Q
(*Qโ๐ฆ) โง ๐ฆ โ Q) โ (๐ฆ
ยทQ ๐ง) <Q (๐ฆ
ยทQ (*Qโ๐ฆ))) |
23 | 22 | expcom 116 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ โ Q โ
(๐ง
<Q (*Qโ๐ฆ) โ (๐ฆ ยทQ ๐ง) <Q
(๐ฆ
ยทQ (*Qโ๐ฆ)))) |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ง
<Q (*Qโ๐ฆ) โ (๐ฆ ยทQ ๐ง) <Q
(๐ฆ
ยทQ (*Qโ๐ฆ)))) |
25 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
26 | | recidnq 7391 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ Q โ
(๐ฆ
ยทQ (*Qโ๐ฆ)) =
1Q) |
27 | 26 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ (*Qโ๐ฆ)) =
1Q) |
28 | 25, 27 | breq12d 4016 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ ((๐ฆ
ยทQ ๐ง) <Q (๐ฆ
ยทQ (*Qโ๐ฆ)) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
29 | 24, 28 | sylibd 149 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ง
<Q (*Qโ๐ฆ) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
30 | 29 | ancoms 268 |
. . . . . . . . . . . . . . . . 17
โข ((๐ง โ Q โง
๐ฆ โ Q)
โ (๐ง
<Q (*Qโ๐ฆ) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
31 | 13, 30 | sylan 283 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
(๐ง
<Q (*Qโ๐ฆ) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
32 | 21, 31 | syld 45 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ (๐ง ยทQ ๐ฆ) <Q
1Q)) |
33 | 17, 32 | anim12d 335 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
((๐
<Q ๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ ((๐ง ยทQ ๐) <Q
(๐ง
ยทQ ๐ฆ) โง (๐ง ยทQ ๐ฆ) <Q
1Q))) |
34 | | ltsonq 7396 |
. . . . . . . . . . . . . . 15
โข
<Q Or Q |
35 | 34, 8 | sotri 5024 |
. . . . . . . . . . . . . 14
โข (((๐ง
ยทQ ๐) <Q (๐ง
ยทQ ๐ฆ) โง (๐ง ยทQ ๐ฆ) <Q
1Q) โ (๐ง ยทQ ๐) <Q
1Q) |
36 | 33, 35 | syl6 33 |
. . . . . . . . . . . . 13
โข (((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โง ๐ฆ โ Q) โ
((๐
<Q ๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ (๐ง ยทQ ๐) <Q
1Q)) |
37 | 36 | exp4b 367 |
. . . . . . . . . . . 12
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ฆ โ Q โ
(๐
<Q ๐ฆ โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ (๐ง ยทQ ๐) <Q
1Q)))) |
38 | 10, 37 | syl5 32 |
. . . . . . . . . . 11
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ <Q
๐ฆ โ (๐ <Q
๐ฆ โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ (๐ง ยทQ ๐) <Q
1Q)))) |
39 | 38 | pm2.43d 50 |
. . . . . . . . . 10
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ <Q
๐ฆ โ
((*Qโ๐ฆ) โ (2nd โ๐ด) โ (๐ง ยทQ ๐) <Q
1Q))) |
40 | 39 | impd 254 |
. . . . . . . . 9
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ ((๐ <Q
๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ (๐ง ยทQ ๐) <Q
1Q)) |
41 | 40 | exlimdv 1819 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ
(โ๐ฆ(๐ <Q
๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด)) โ (๐ง ยทQ ๐) <Q
1Q)) |
42 | 7, 41 | biimtrid 152 |
. . . . . . 7
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ โ (1st
โ๐ต) โ (๐ง
ยทQ ๐) <Q
1Q)) |
43 | | breq1 4006 |
. . . . . . . 8
โข (๐ค = (๐ง ยทQ ๐) โ (๐ค <Q
1Q โ (๐ง ยทQ ๐) <Q
1Q)) |
44 | 43 | biimprcd 160 |
. . . . . . 7
โข ((๐ง
ยทQ ๐) <Q
1Q โ (๐ค = (๐ง ยทQ ๐) โ ๐ค <Q
1Q)) |
45 | 42, 44 | syl6 33 |
. . . . . 6
โข ((๐ด โ P โง
๐ง โ (1st
โ๐ด)) โ (๐ โ (1st
โ๐ต) โ (๐ค = (๐ง ยทQ ๐) โ ๐ค <Q
1Q))) |
46 | 45 | expimpd 363 |
. . . . 5
โข (๐ด โ P โ
((๐ง โ (1st
โ๐ด) โง ๐ โ (1st
โ๐ต)) โ (๐ค = (๐ง ยทQ ๐) โ ๐ค <Q
1Q))) |
47 | 46 | rexlimdvv 2601 |
. . . 4
โข (๐ด โ P โ
(โ๐ง โ
(1st โ๐ด)โ๐ โ (1st โ๐ต)๐ค = (๐ง ยทQ ๐) โ ๐ค <Q
1Q)) |
48 | 6, 47 | sylbid 150 |
. . 3
โข (๐ด โ P โ
(๐ค โ (1st
โ(๐ด
ยทP ๐ต)) โ ๐ค <Q
1Q)) |
49 | | 1prl 7553 |
. . . 4
โข
(1st โ1P) = {๐ค โฃ ๐ค <Q
1Q} |
50 | 49 | abeq2i 2288 |
. . 3
โข (๐ค โ (1st
โ1P) โ ๐ค <Q
1Q) |
51 | 48, 50 | syl6ibr 162 |
. 2
โข (๐ด โ P โ
(๐ค โ (1st
โ(๐ด
ยทP ๐ต)) โ ๐ค โ (1st
โ1P))) |
52 | 51 | ssrdv 3161 |
1
โข (๐ด โ P โ
(1st โ(๐ด
ยทP ๐ต)) โ (1st
โ1P)) |