Step | Hyp | Ref
| Expression |
1 | | ssid 3175 |
. . . . . 6
โข
(2nd โ1P) โ
(2nd โ1P) |
2 | | rexss 3222 |
. . . . . 6
โข
((2nd โ1P) โ
(2nd โ1P) โ (โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ) โ โโ โ (2nd
โ1P)(โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ)))) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
โข
(โโ โ
(2nd โ1P)๐ฅ = (๐ ยทQ โ) โ โโ โ (2nd
โ1P)(โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ))) |
4 | | 1pr 7552 |
. . . . . . . . . . 11
โข
1P โ P |
5 | | prop 7473 |
. . . . . . . . . . . 12
โข
(1P โ P โ
โจ(1st โ1P), (2nd
โ1P)โฉ โ
P) |
6 | | elprnqu 7480 |
. . . . . . . . . . . 12
โข
((โจ(1st โ1P),
(2nd โ1P)โฉ โ
P โง โ
โ (2nd โ1P)) โ โ โ
Q) |
7 | 5, 6 | sylan 283 |
. . . . . . . . . . 11
โข
((1P โ P โง โ โ (2nd
โ1P)) โ โ โ Q) |
8 | 4, 7 | mpan 424 |
. . . . . . . . . 10
โข (โ โ (2nd
โ1P) โ โ โ Q) |
9 | | prop 7473 |
. . . . . . . . . . . 12
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
10 | | elprnqu 7480 |
. . . . . . . . . . . 12
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ โ (2nd
โ๐ด)) โ ๐ โ
Q) |
11 | 9, 10 | sylan 283 |
. . . . . . . . . . 11
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ ๐ โ
Q) |
12 | | breq2 4007 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ ยทQ โ) โ (๐ <Q ๐ฅ โ ๐ <Q (๐
ยทQ โ))) |
13 | 12 | 3ad2ant3 1020 |
. . . . . . . . . . . 12
โข ((๐ โ Q โง
โ โ Q
โง ๐ฅ = (๐
ยทQ โ)) โ (๐ <Q ๐ฅ โ ๐ <Q (๐
ยทQ โ))) |
14 | | 1pru 7554 |
. . . . . . . . . . . . . . 15
โข
(2nd โ1P) = {โ โฃ
1Q <Q โ} |
15 | 14 | abeq2i 2288 |
. . . . . . . . . . . . . 14
โข (โ โ (2nd
โ1P) โ 1Q
<Q โ) |
16 | | 1nq 7364 |
. . . . . . . . . . . . . . . . 17
โข
1Q โ Q |
17 | | ltmnqg 7399 |
. . . . . . . . . . . . . . . . 17
โข
((1Q โ Q โง โ โ Q โง
๐ โ Q)
โ (1Q <Q โ โ (๐ ยทQ
1Q) <Q (๐ ยทQ โ))) |
18 | 16, 17 | mp3an1 1324 |
. . . . . . . . . . . . . . . 16
โข ((โ โ Q โง
๐ โ Q)
โ (1Q <Q โ โ (๐ ยทQ
1Q) <Q (๐ ยทQ โ))) |
19 | 18 | ancoms 268 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
โ โ Q)
โ (1Q <Q โ โ (๐ ยทQ
1Q) <Q (๐ ยทQ โ))) |
20 | | mulidnq 7387 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
21 | 20 | breq1d 4013 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
((๐
ยทQ 1Q)
<Q (๐ ยทQ โ) โ ๐ <Q (๐
ยทQ โ))) |
22 | 21 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
โ โ Q)
โ ((๐
ยทQ 1Q)
<Q (๐ ยทQ โ) โ ๐ <Q (๐
ยทQ โ))) |
23 | 19, 22 | bitrd 188 |
. . . . . . . . . . . . . 14
โข ((๐ โ Q โง
โ โ Q)
โ (1Q <Q โ โ ๐ <Q (๐
ยทQ โ))) |
24 | 15, 23 | bitr2id 193 |
. . . . . . . . . . . . 13
โข ((๐ โ Q โง
โ โ Q)
โ (๐
<Q (๐ ยทQ โ) โ โ โ (2nd
โ1P))) |
25 | 24 | 3adant3 1017 |
. . . . . . . . . . . 12
โข ((๐ โ Q โง
โ โ Q
โง ๐ฅ = (๐
ยทQ โ)) โ (๐ <Q (๐
ยทQ โ) โ โ โ (2nd
โ1P))) |
26 | 13, 25 | bitrd 188 |
. . . . . . . . . . 11
โข ((๐ โ Q โง
โ โ Q
โง ๐ฅ = (๐
ยทQ โ)) โ (๐ <Q ๐ฅ โ โ โ (2nd
โ1P))) |
27 | 11, 26 | syl3an1 1271 |
. . . . . . . . . 10
โข (((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โง โ โ Q โง
๐ฅ = (๐ ยทQ โ)) โ (๐ <Q ๐ฅ โ โ โ (2nd
โ1P))) |
28 | 8, 27 | syl3an2 1272 |
. . . . . . . . 9
โข (((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โง โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ)) โ (๐ <Q ๐ฅ โ โ โ (2nd
โ1P))) |
29 | 28 | 3expia 1205 |
. . . . . . . 8
โข (((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โง โ โ (2nd
โ1P)) โ (๐ฅ = (๐ ยทQ โ) โ (๐ <Q ๐ฅ โ โ โ (2nd
โ1P)))) |
30 | 29 | pm5.32rd 451 |
. . . . . . 7
โข (((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โง โ โ (2nd
โ1P)) โ ((๐ <Q ๐ฅ โง ๐ฅ = (๐ ยทQ โ)) โ (โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ)))) |
31 | 30 | rexbidva 2474 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ
(โโ โ
(2nd โ1P)(๐ <Q ๐ฅ โง ๐ฅ = (๐ ยทQ โ)) โ โโ โ (2nd
โ1P)(โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ)))) |
32 | | r19.42v 2634 |
. . . . . 6
โข
(โโ โ
(2nd โ1P)(๐ <Q ๐ฅ โง ๐ฅ = (๐ ยทQ โ)) โ (๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
33 | 31, 32 | bitr3di 195 |
. . . . 5
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ
(โโ โ
(2nd โ1P)(โ โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ โ)) โ (๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)))) |
34 | 3, 33 | bitrid 192 |
. . . 4
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ
(โโ โ
(2nd โ1P)๐ฅ = (๐ ยทQ โ) โ (๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)))) |
35 | 34 | rexbidva 2474 |
. . 3
โข (๐ด โ P โ
(โ๐ โ
(2nd โ๐ด)โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ) โ โ๐ โ (2nd
โ๐ด)(๐ <Q
๐ฅ โง โโ โ (2nd
โ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 | genpelvu 7511 |
. . . 4
โข ((๐ด โ P โง
1P โ P) โ (๐ฅ โ (2nd โ(๐ด
ยทP 1P)) โ
โ๐ โ
(2nd โ๐ด)โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
39 | 4, 38 | mpan2 425 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ (2nd
โ(๐ด
ยทP 1P)) โ
โ๐ โ
(2nd โ๐ด)โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
40 | | prnminu 7487 |
. . . . . . 7
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ฅ โ (2nd
โ๐ด)) โ
โ๐ โ
(2nd โ๐ด)๐ <Q ๐ฅ) |
41 | 9, 40 | sylan 283 |
. . . . . 6
โข ((๐ด โ P โง
๐ฅ โ (2nd
โ๐ด)) โ
โ๐ โ
(2nd โ๐ด)๐ <Q ๐ฅ) |
42 | | ltrelnq 7363 |
. . . . . . . . . . . . . 14
โข
<Q โ (Q ร
Q) |
43 | 42 | brel 4678 |
. . . . . . . . . . . . 13
โข (๐ <Q
๐ฅ โ (๐ โ Q โง
๐ฅ โ
Q)) |
44 | 43 | ancomd 267 |
. . . . . . . . . . . 12
โข (๐ <Q
๐ฅ โ (๐ฅ โ Q โง
๐ โ
Q)) |
45 | | ltmnqg 7399 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ Q โง
๐ง โ Q
โง ๐ค โ
Q) โ (๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
46 | 45 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ Q โง
๐ โ Q)
โง (๐ฆ โ
Q โง ๐ง
โ Q โง ๐ค โ Q)) โ (๐ฆ <Q
๐ง โ (๐ค
ยทQ ๐ฆ) <Q (๐ค
ยทQ ๐ง))) |
47 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ โ
Q) |
48 | | simpl 109 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ฅ โ
Q) |
49 | | recclnq 7390 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
(*Qโ๐) โ Q) |
50 | 49 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (*Qโ๐) โ Q) |
51 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
52 | 51 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ Q โง
๐ โ Q)
โง (๐ฆ โ
Q โง ๐ง
โ Q)) โ (๐ฆ ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
53 | 46, 47, 48, 50, 52 | caovord2d 6043 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
<Q ๐ฅ โ (๐ ยทQ
(*Qโ๐)) <Q (๐ฅ
ยทQ (*Qโ๐)))) |
54 | | recidnq 7391 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Q โ
(๐
ยทQ (*Qโ๐)) =
1Q) |
55 | 54 | breq1d 4013 |
. . . . . . . . . . . . . . 15
โข (๐ โ Q โ
((๐
ยทQ (*Qโ๐))
<Q (๐ฅ ยทQ
(*Qโ๐)) โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
56 | 55 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ((๐
ยทQ (*Qโ๐))
<Q (๐ฅ ยทQ
(*Qโ๐)) โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
57 | 53, 56 | bitrd 188 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
<Q ๐ฅ โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
58 | 57 | biimpd 144 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
<Q ๐ฅ โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
59 | 44, 58 | mpcom 36 |
. . . . . . . . . . 11
โข (๐ <Q
๐ฅ โ
1Q <Q (๐ฅ ยทQ
(*Qโ๐))) |
60 | | mulclnq 7374 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ Q โง
(*Qโ๐) โ Q) โ (๐ฅ
ยทQ (*Qโ๐)) โ
Q) |
61 | 49, 60 | sylan2 286 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ
ยทQ (*Qโ๐)) โ
Q) |
62 | | breq2 4007 |
. . . . . . . . . . . . 13
โข (โ = (๐ฅ ยทQ
(*Qโ๐)) โ (1Q
<Q โ โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
63 | 62, 14 | elab2g 2884 |
. . . . . . . . . . . 12
โข ((๐ฅ
ยทQ (*Qโ๐)) โ Q โ
((๐ฅ
ยทQ (*Qโ๐)) โ (2nd
โ1P) โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
64 | 44, 61, 63 | 3syl 17 |
. . . . . . . . . . 11
โข (๐ <Q
๐ฅ โ ((๐ฅ
ยทQ (*Qโ๐)) โ (2nd
โ1P) โ 1Q
<Q (๐ฅ ยทQ
(*Qโ๐)))) |
65 | 59, 64 | mpbird 167 |
. . . . . . . . . 10
โข (๐ <Q
๐ฅ โ (๐ฅ
ยทQ (*Qโ๐)) โ (2nd
โ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, 48, 50, 52, 67 | caov12d 6055 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ (๐
ยทQ (*Qโ๐)))) |
69 | 54 | 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 | 44, 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โ๐)) โ (2nd
โ1P) โง ๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐)))) โ โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)) |
78 | 65, 74, 77 | syl2anc 411 |
. . . . . . . . 9
โข (๐ <Q
๐ฅ โ โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)) |
79 | 78 | a1i 9 |
. . . . . . . 8
โข (๐ โ (2nd
โ๐ด) โ (๐ <Q
๐ฅ โ โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
80 | 79 | ancld 325 |
. . . . . . 7
โข (๐ โ (2nd
โ๐ด) โ (๐ <Q
๐ฅ โ (๐ <Q
๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)))) |
81 | 80 | reximia 2572 |
. . . . . 6
โข
(โ๐ โ
(2nd โ๐ด)๐ <Q ๐ฅ โ โ๐ โ (2nd
โ๐ด)(๐ <Q
๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
82 | 41, 81 | syl 14 |
. . . . 5
โข ((๐ด โ P โง
๐ฅ โ (2nd
โ๐ด)) โ
โ๐ โ
(2nd โ๐ด)(๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ))) |
83 | 82 | ex 115 |
. . . 4
โข (๐ด โ P โ
(๐ฅ โ (2nd
โ๐ด) โ
โ๐ โ
(2nd โ๐ด)(๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)))) |
84 | | prcunqu 7483 |
. . . . . . 7
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ โ (2nd
โ๐ด)) โ (๐ <Q
๐ฅ โ ๐ฅ โ (2nd โ๐ด))) |
85 | 9, 84 | sylan 283 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ (๐ <Q
๐ฅ โ ๐ฅ โ (2nd โ๐ด))) |
86 | 85 | adantrd 279 |
. . . . 5
โข ((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โ ((๐ <Q
๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)) โ ๐ฅ โ (2nd โ๐ด))) |
87 | 86 | rexlimdva 2594 |
. . . 4
โข (๐ด โ P โ
(โ๐ โ
(2nd โ๐ด)(๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)) โ ๐ฅ โ (2nd โ๐ด))) |
88 | 83, 87 | impbid 129 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ (2nd
โ๐ด) โ
โ๐ โ
(2nd โ๐ด)(๐ <Q ๐ฅ โง โโ โ (2nd
โ1P)๐ฅ = (๐ ยทQ โ)))) |
89 | 35, 39, 88 | 3bitr4d 220 |
. 2
โข (๐ด โ P โ
(๐ฅ โ (2nd
โ(๐ด
ยทP 1P)) โ ๐ฅ โ (2nd
โ๐ด))) |
90 | 89 | eqrdv 2175 |
1
โข (๐ด โ P โ
(2nd โ(๐ด
ยทP 1P)) =
(2nd โ๐ด)) |