Step | Hyp | Ref
| Expression |
1 | | ssid 3175 |
. . . . . 6
โข
(1st โ1P) โ
(1st โ1P) |
2 | | rexss 3222 |
. . . . . 6
โข
((1st โ1P) โ
(1st โ1P) โ (โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐) โ โ๐ โ (1st
โ1P)(๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐)))) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
โข
(โ๐ โ
(1st โ1P)๐ฅ = (๐ ยทQ ๐) โ โ๐ โ (1st
โ1P)(๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐))) |
4 | | 1pr 7552 |
. . . . . . . . . . 11
โข
1P โ P |
5 | | prop 7473 |
. . . . . . . . . . . 12
โข
(1P โ P โ
โจ(1st โ1P), (2nd
โ1P)โฉ โ
P) |
6 | | elprnql 7479 |
. . . . . . . . . . . 12
โข
((โจ(1st โ1P),
(2nd โ1P)โฉ โ
P โง ๐
โ (1st โ1P)) โ ๐ โ
Q) |
7 | 5, 6 | sylan 283 |
. . . . . . . . . . 11
โข
((1P โ P โง ๐ โ (1st
โ1P)) โ ๐ โ Q) |
8 | 4, 7 | mpan 424 |
. . . . . . . . . 10
โข (๐ โ (1st
โ1P) โ ๐ โ Q) |
9 | | prop 7473 |
. . . . . . . . . . . 12
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
10 | | elprnql 7479 |
. . . . . . . . . . . 12
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ โ (1st
โ๐ด)) โ ๐ โ
Q) |
11 | 9, 10 | sylan 283 |
. . . . . . . . . . 11
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ ๐ โ
Q) |
12 | | breq1 4006 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โ (๐ ยทQ ๐) <Q
๐)) |
13 | 12 | 3ad2ant3 1020 |
. . . . . . . . . . . 12
โข ((๐ โ Q โง
๐ โ Q
โง ๐ฅ = (๐
ยทQ ๐)) โ (๐ฅ <Q ๐ โ (๐ ยทQ ๐) <Q
๐)) |
14 | | 1prl 7553 |
. . . . . . . . . . . . . . 15
โข
(1st โ1P) = {๐ โฃ ๐ <Q
1Q} |
15 | 14 | abeq2i 2288 |
. . . . . . . . . . . . . 14
โข (๐ โ (1st
โ1P) โ ๐ <Q
1Q) |
16 | | 1nq 7364 |
. . . . . . . . . . . . . . . . 17
โข
1Q โ Q |
17 | | ltmnqg 7399 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ Q โง
1Q โ Q โง ๐ โ Q) โ (๐ <Q
1Q โ (๐ ยทQ ๐) <Q
(๐
ยทQ
1Q))) |
18 | 16, 17 | mp3an2 1325 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
<Q 1Q โ (๐
ยทQ ๐) <Q (๐
ยทQ
1Q))) |
19 | 18 | ancoms 268 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
<Q 1Q โ (๐
ยทQ ๐) <Q (๐
ยทQ
1Q))) |
20 | | mulidnq 7387 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
21 | 20 | breq2d 4015 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
((๐
ยทQ ๐) <Q (๐
ยทQ 1Q) โ (๐
ยทQ ๐) <Q ๐)) |
22 | 21 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
๐ โ Q)
โ ((๐
ยทQ ๐) <Q (๐
ยทQ 1Q) โ (๐
ยทQ ๐) <Q ๐)) |
23 | 19, 22 | bitrd 188 |
. . . . . . . . . . . . . 14
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
<Q 1Q โ (๐
ยทQ ๐) <Q ๐)) |
24 | 15, 23 | bitr2id 193 |
. . . . . . . . . . . . 13
โข ((๐ โ Q โง
๐ โ Q)
โ ((๐
ยทQ ๐) <Q ๐ โ ๐ โ (1st
โ1P))) |
25 | 24 | 3adant3 1017 |
. . . . . . . . . . . 12
โข ((๐ โ Q โง
๐ โ Q
โง ๐ฅ = (๐
ยทQ ๐)) โ ((๐ ยทQ ๐) <Q
๐ โ ๐ โ (1st
โ1P))) |
26 | 13, 25 | bitrd 188 |
. . . . . . . . . . 11
โข ((๐ โ Q โง
๐ โ Q
โง ๐ฅ = (๐
ยทQ ๐)) โ (๐ฅ <Q ๐ โ ๐ โ (1st
โ1P))) |
27 | 11, 26 | syl3an1 1271 |
. . . . . . . . . 10
โข (((๐ด โ P โง
๐ โ (1st
โ๐ด)) โง ๐ โ Q โง
๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โ ๐ โ (1st
โ1P))) |
28 | 8, 27 | syl3an2 1272 |
. . . . . . . . 9
โข (((๐ด โ P โง
๐ โ (1st
โ๐ด)) โง ๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โ ๐ โ (1st
โ1P))) |
29 | 28 | 3expia 1205 |
. . . . . . . 8
โข (((๐ด โ P โง
๐ โ (1st
โ๐ด)) โง ๐ โ (1st
โ1P)) โ (๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โ ๐ โ (1st
โ1P)))) |
30 | 29 | pm5.32rd 451 |
. . . . . . 7
โข (((๐ด โ P โง
๐ โ (1st
โ๐ด)) โง ๐ โ (1st
โ1P)) โ ((๐ฅ <Q ๐ โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐)))) |
31 | 30 | rexbidva 2474 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ
(โ๐ โ
(1st โ1P)(๐ฅ <Q ๐ โง ๐ฅ = (๐ ยทQ ๐)) โ โ๐ โ (1st
โ1P)(๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐)))) |
32 | | r19.42v 2634 |
. . . . . 6
โข
(โ๐ โ
(1st โ1P)(๐ฅ <Q ๐ โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
33 | 31, 32 | bitr3di 195 |
. . . . 5
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ
(โ๐ โ
(1st โ1P)(๐ โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
34 | 3, 33 | bitrid 192 |
. . . 4
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ
(โ๐ โ
(1st โ1P)๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
35 | 34 | rexbidva 2474 |
. . 3
โข (๐ด โ P โ
(โ๐ โ
(1st โ๐ด)โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐) โ โ๐ โ (1st
โ๐ด)(๐ฅ <Q
๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
36 | | df-imp 7467 |
. . . . 5
โข
ยทP = (๐ฆ โ P, ๐ง โ P โฆ โจ{๐ค โ Q โฃ
โ๐ข โ
Q โ๐ฃ
โ Q (๐ข
โ (1st โ๐ฆ) โง ๐ฃ โ (1st โ๐ง) โง ๐ค = (๐ข ยทQ ๐ฃ))}, {๐ค โ Q โฃ โ๐ข โ Q
โ๐ฃ โ
Q (๐ข โ
(2nd โ๐ฆ)
โง ๐ฃ โ
(2nd โ๐ง)
โง ๐ค = (๐ข
ยทQ ๐ฃ))}โฉ) |
37 | | mulclnq 7374 |
. . . . 5
โข ((๐ข โ Q โง
๐ฃ โ Q)
โ (๐ข
ยทQ ๐ฃ) โ Q) |
38 | 36, 37 | genpelvl 7510 |
. . . 4
โข ((๐ด โ P โง
1P โ P) โ (๐ฅ โ (1st โ(๐ด
ยทP 1P)) โ
โ๐ โ
(1st โ๐ด)โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
39 | 4, 38 | mpan2 425 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ (1st
โ(๐ด
ยทP 1P)) โ
โ๐ โ
(1st โ๐ด)โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
40 | | prnmaxl 7486 |
. . . . . . 7
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ฅ โ (1st
โ๐ด)) โ
โ๐ โ
(1st โ๐ด)๐ฅ <Q ๐) |
41 | 9, 40 | sylan 283 |
. . . . . 6
โข ((๐ด โ P โง
๐ฅ โ (1st
โ๐ด)) โ
โ๐ โ
(1st โ๐ด)๐ฅ <Q ๐) |
42 | | ltrelnq 7363 |
. . . . . . . . . . . . 13
โข
<Q โ (Q ร
Q) |
43 | 42 | brel 4678 |
. . . . . . . . . . . 12
โข (๐ฅ <Q
๐ โ (๐ฅ โ Q โง
๐ โ
Q)) |
44 | | ltmnqg 7399 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ Q โง
๐ง โ Q
โง ๐ค โ
Q) โ (๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
45 | 44 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ Q โง
๐ โ Q)
โง (๐ฆ โ
Q โง ๐ง
โ Q โง ๐ค โ Q)) โ (๐ฆ <Q
๐ง โ (๐ค
ยทQ ๐ฆ) <Q (๐ค
ยทQ ๐ง))) |
46 | | simpl 109 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ฅ โ
Q) |
47 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ โ
Q) |
48 | | recclnq 7390 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
(*Qโ๐) โ Q) |
49 | 48 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (*Qโ๐) โ Q) |
50 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
51 | 50 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ Q โง
๐ โ Q)
โง (๐ฆ โ
Q โง ๐ง
โ Q)) โ (๐ฆ ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
52 | 45, 46, 47, 49, 51 | caovord2d 6043 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
<Q ๐ โ (๐ฅ ยทQ
(*Qโ๐)) <Q (๐
ยทQ (*Qโ๐)))) |
53 | | recidnq 7391 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
(๐
ยทQ (*Qโ๐)) =
1Q) |
54 | 53 | breq2d 4015 |
. . . . . . . . . . . . . . 15
โข (๐ โ Q โ
((๐ฅ
ยทQ (*Qโ๐))
<Q (๐ ยทQ
(*Qโ๐)) โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
55 | 54 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ((๐ฅ
ยทQ (*Qโ๐))
<Q (๐ ยทQ
(*Qโ๐)) โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
56 | 52, 55 | bitrd 188 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
<Q ๐ โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
57 | 56 | biimpd 144 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
<Q ๐ โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
58 | 43, 57 | mpcom 36 |
. . . . . . . . . . 11
โข (๐ฅ <Q
๐ โ (๐ฅ
ยทQ (*Qโ๐))
<Q 1Q) |
59 | | mulclnq 7374 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Q โง
(*Qโ๐) โ Q) โ (๐ฅ
ยทQ (*Qโ๐)) โ
Q) |
60 | 48, 59 | sylan2 286 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
ยทQ (*Qโ๐)) โ
Q) |
61 | 43, 60 | syl 14 |
. . . . . . . . . . . 12
โข (๐ฅ <Q
๐ โ (๐ฅ
ยทQ (*Qโ๐)) โ
Q) |
62 | | breq1 4006 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ ยทQ
(*Qโ๐)) โ (๐ <Q
1Q โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
63 | 62, 14 | elab2g 2884 |
. . . . . . . . . . . 12
โข ((๐ฅ
ยทQ (*Qโ๐)) โ Q โ
((๐ฅ
ยทQ (*Qโ๐)) โ (1st
โ1P) โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
64 | 61, 63 | syl 14 |
. . . . . . . . . . 11
โข (๐ฅ <Q
๐ โ ((๐ฅ
ยทQ (*Qโ๐)) โ (1st
โ1P) โ (๐ฅ ยทQ
(*Qโ๐)) <Q
1Q)) |
65 | 58, 64 | mpbird 167 |
. . . . . . . . . 10
โข (๐ฅ <Q
๐ โ (๐ฅ
ยทQ (*Qโ๐)) โ (1st
โ1P)) |
66 | | mulassnqg 7382 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ Q โง
๐ง โ Q
โง ๐ค โ
Q) โ ((๐ฆ
ยทQ ๐ง) ยทQ ๐ค) = (๐ฆ ยทQ (๐ง
ยทQ ๐ค))) |
67 | 66 | adantl 277 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ Q โง
๐ โ Q)
โง (๐ฆ โ
Q โง ๐ง
โ Q โง ๐ค โ Q)) โ ((๐ฆ
ยทQ ๐ง) ยทQ ๐ค) = (๐ฆ ยทQ (๐ง
ยทQ ๐ค))) |
68 | 47, 46, 49, 51, 67 | caov12d 6055 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ (๐
ยทQ (*Qโ๐)))) |
69 | 53 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข (๐ โ Q โ
(๐ฅ
ยทQ (๐ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ
1Q)) |
70 | 69 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
ยทQ (๐ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ
1Q)) |
71 | | mulidnq 7387 |
. . . . . . . . . . . . 13
โข (๐ฅ โ Q โ
(๐ฅ
ยทQ 1Q) = ๐ฅ) |
72 | 71 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
ยทQ 1Q) = ๐ฅ) |
73 | 68, 70, 72 | 3eqtrrd 2215 |
. . . . . . . . . . 11
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ฅ = (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐)))) |
74 | 43, 73 | syl 14 |
. . . . . . . . . 10
โข (๐ฅ <Q
๐ โ ๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐)))) |
75 | | oveq2 5882 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ ยทQ
(*Qโ๐)) โ (๐ ยทQ ๐) = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐)))) |
76 | 75 | eqeq2d 2189 |
. . . . . . . . . . 11
โข (๐ = (๐ฅ ยทQ
(*Qโ๐)) โ (๐ฅ = (๐ ยทQ ๐) โ ๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐))))) |
77 | 76 | rspcev 2841 |
. . . . . . . . . 10
โข (((๐ฅ
ยทQ (*Qโ๐)) โ (1st
โ1P) โง ๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐)))) โ โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)) |
78 | 65, 74, 77 | syl2anc 411 |
. . . . . . . . 9
โข (๐ฅ <Q
๐ โ โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)) |
79 | 78 | a1i 9 |
. . . . . . . 8
โข (๐ โ (1st
โ๐ด) โ (๐ฅ <Q
๐ โ โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
80 | 79 | ancld 325 |
. . . . . . 7
โข (๐ โ (1st
โ๐ด) โ (๐ฅ <Q
๐ โ (๐ฅ <Q
๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
81 | 80 | reximia 2572 |
. . . . . 6
โข
(โ๐ โ
(1st โ๐ด)๐ฅ <Q ๐ โ โ๐ โ (1st
โ๐ด)(๐ฅ <Q
๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
82 | 41, 81 | syl 14 |
. . . . 5
โข ((๐ด โ P โง
๐ฅ โ (1st
โ๐ด)) โ
โ๐ โ
(1st โ๐ด)(๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐))) |
83 | 82 | ex 115 |
. . . 4
โข (๐ด โ P โ
(๐ฅ โ (1st
โ๐ด) โ
โ๐ โ
(1st โ๐ด)(๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
84 | | prcdnql 7482 |
. . . . . . 7
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ โ (1st
โ๐ด)) โ (๐ฅ <Q
๐ โ ๐ฅ โ (1st โ๐ด))) |
85 | 9, 84 | sylan 283 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ (๐ฅ <Q
๐ โ ๐ฅ โ (1st โ๐ด))) |
86 | 85 | adantrd 279 |
. . . . 5
โข ((๐ด โ P โง
๐ โ (1st
โ๐ด)) โ ((๐ฅ <Q
๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)) โ ๐ฅ โ (1st โ๐ด))) |
87 | 86 | rexlimdva 2594 |
. . . 4
โข (๐ด โ P โ
(โ๐ โ
(1st โ๐ด)(๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)) โ ๐ฅ โ (1st โ๐ด))) |
88 | 83, 87 | impbid 129 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ (1st
โ๐ด) โ
โ๐ โ
(1st โ๐ด)(๐ฅ <Q ๐ โง โ๐ โ (1st
โ1P)๐ฅ = (๐ ยทQ ๐)))) |
89 | 35, 39, 88 | 3bitr4d 220 |
. 2
โข (๐ด โ P โ
(๐ฅ โ (1st
โ(๐ด
ยทP 1P)) โ ๐ฅ โ (1st
โ๐ด))) |
90 | 89 | eqrdv 2175 |
1
โข (๐ด โ P โ
(1st โ(๐ด
ยทP 1P)) =
(1st โ๐ด)) |