Step | Hyp | Ref
| Expression |
1 | | pospo.s |
. . . . 5
β’ < =
(ltβπΎ) |
2 | 1 | pltirr 18288 |
. . . 4
β’ ((πΎ β Poset β§ π₯ β π΅) β Β¬ π₯ < π₯) |
3 | | pospo.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
4 | 3, 1 | plttr 18295 |
. . . 4
β’ ((πΎ β Poset β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ < π¦ β§ π¦ < π§) β π₯ < π§)) |
5 | 2, 4 | ispod 5598 |
. . 3
β’ (πΎ β Poset β < Po π΅) |
6 | | relres 6011 |
. . . . 5
β’ Rel ( I
βΎ π΅) |
7 | 6 | a1i 11 |
. . . 4
β’ (πΎ β Poset β Rel ( I
βΎ π΅)) |
8 | | opabresid 6050 |
. . . . . . . 8
β’ ( I
βΎ π΅) = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ = π₯)} |
9 | 8 | eqcomi 2742 |
. . . . . . 7
β’
{β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ = π₯)} = ( I βΎ π΅) |
10 | 9 | eleq2i 2826 |
. . . . . 6
β’
(β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ = π₯)} β β¨π₯, π¦β© β ( I βΎ π΅)) |
11 | | opabidw 5525 |
. . . . . 6
β’
(β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ = π₯)} β (π₯ β π΅ β§ π¦ = π₯)) |
12 | 10, 11 | bitr3i 277 |
. . . . 5
β’
(β¨π₯, π¦β© β ( I βΎ π΅) β (π₯ β π΅ β§ π¦ = π₯)) |
13 | | pospo.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
14 | 3, 13 | posref 18271 |
. . . . . . 7
β’ ((πΎ β Poset β§ π₯ β π΅) β π₯ β€ π₯) |
15 | | df-br 5150 |
. . . . . . . 8
β’ (π₯ β€ π¦ β β¨π₯, π¦β© β β€ ) |
16 | | breq2 5153 |
. . . . . . . 8
β’ (π¦ = π₯ β (π₯ β€ π¦ β π₯ β€ π₯)) |
17 | 15, 16 | bitr3id 285 |
. . . . . . 7
β’ (π¦ = π₯ β (β¨π₯, π¦β© β β€ β π₯ β€ π₯)) |
18 | 14, 17 | syl5ibrcom 246 |
. . . . . 6
β’ ((πΎ β Poset β§ π₯ β π΅) β (π¦ = π₯ β β¨π₯, π¦β© β β€ )) |
19 | 18 | expimpd 455 |
. . . . 5
β’ (πΎ β Poset β ((π₯ β π΅ β§ π¦ = π₯) β β¨π₯, π¦β© β β€ )) |
20 | 12, 19 | biimtrid 241 |
. . . 4
β’ (πΎ β Poset β
(β¨π₯, π¦β© β ( I βΎ π΅) β β¨π₯, π¦β© β β€ )) |
21 | 7, 20 | relssdv 5789 |
. . 3
β’ (πΎ β Poset β ( I βΎ
π΅) β β€
) |
22 | 5, 21 | jca 513 |
. 2
β’ (πΎ β Poset β ( < Po π΅ β§ ( I βΎ π΅) β β€ )) |
23 | | simpl 484 |
. . . 4
β’ ((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β πΎ β π) |
24 | 3 | a1i 11 |
. . . 4
β’ ((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β π΅ = (BaseβπΎ)) |
25 | 13 | a1i 11 |
. . . 4
β’ ((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β β€ =
(leβπΎ)) |
26 | | equid 2016 |
. . . . . 6
β’ π₯ = π₯ |
27 | | simpr 486 |
. . . . . . 7
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β π₯ β π΅) |
28 | | resieq 5993 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π₯ β π΅) β (π₯( I βΎ π΅)π₯ β π₯ = π₯)) |
29 | 27, 27, 28 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β (π₯( I βΎ π΅)π₯ β π₯ = π₯)) |
30 | 26, 29 | mpbiri 258 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β π₯( I βΎ π΅)π₯) |
31 | | simplrr 777 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β ( I βΎ π΅) β β€ ) |
32 | 31 | ssbrd 5192 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β (π₯( I βΎ π΅)π₯ β π₯ β€ π₯)) |
33 | 30, 32 | mpd 15 |
. . . 4
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅) β π₯ β€ π₯) |
34 | 3, 13, 1 | pleval2i 18289 |
. . . . . 6
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ β€ π¦ β (π₯ < π¦ β¨ π₯ = π¦))) |
35 | 34 | 3adant1 1131 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ β€ π¦ β (π₯ < π¦ β¨ π₯ = π¦))) |
36 | 3, 13, 1 | pleval2i 18289 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ β π΅) β (π¦ β€ π₯ β (π¦ < π₯ β¨ π¦ = π₯))) |
37 | 36 | ancoms 460 |
. . . . . 6
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π¦ β€ π₯ β (π¦ < π₯ β¨ π¦ = π₯))) |
38 | 37 | 3adant1 1131 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β (π¦ β€ π₯ β (π¦ < π₯ β¨ π¦ = π₯))) |
39 | | simprl 770 |
. . . . . . . 8
β’ ((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β < Po π΅) |
40 | | po2nr 5603 |
. . . . . . . . 9
β’ (( < Po π΅ β§ (π₯ β π΅ β§ π¦ β π΅)) β Β¬ (π₯ < π¦ β§ π¦ < π₯)) |
41 | 40 | 3impb 1116 |
. . . . . . . 8
β’ (( < Po π΅ β§ π₯ β π΅ β§ π¦ β π΅) β Β¬ (π₯ < π¦ β§ π¦ < π₯)) |
42 | 39, 41 | syl3an1 1164 |
. . . . . . 7
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β Β¬ (π₯ < π¦ β§ π¦ < π₯)) |
43 | 42 | pm2.21d 121 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ < π¦ β§ π¦ < π₯) β π₯ = π¦)) |
44 | | simpl 484 |
. . . . . . 7
β’ ((π₯ = π¦ β§ π¦ < π₯) β π₯ = π¦) |
45 | 44 | a1i 11 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ = π¦ β§ π¦ < π₯) β π₯ = π¦)) |
46 | | simpr 486 |
. . . . . . . 8
β’ ((π₯ < π¦ β§ π¦ = π₯) β π¦ = π₯) |
47 | 46 | equcomd 2023 |
. . . . . . 7
β’ ((π₯ < π¦ β§ π¦ = π₯) β π₯ = π¦) |
48 | 47 | a1i 11 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ < π¦ β§ π¦ = π₯) β π₯ = π¦)) |
49 | | simpl 484 |
. . . . . . 7
β’ ((π₯ = π¦ β§ π¦ = π₯) β π₯ = π¦) |
50 | 49 | a1i 11 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ = π¦ β§ π¦ = π₯) β π₯ = π¦)) |
51 | 43, 45, 48, 50 | ccased 1038 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β (((π₯ < π¦ β¨ π₯ = π¦) β§ (π¦ < π₯ β¨ π¦ = π₯)) β π₯ = π¦)) |
52 | 35, 38, 51 | syl2and 609 |
. . . 4
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ π₯ β π΅ β§ π¦ β π΅) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦)) |
53 | | simpr1 1195 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π₯ β π΅) |
54 | | simpr2 1196 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
55 | 53, 54, 34 | syl2anc 585 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β€ π¦ β (π₯ < π¦ β¨ π₯ = π¦))) |
56 | | simpr3 1197 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π§ β π΅) |
57 | 3, 13, 1 | pleval2i 18289 |
. . . . . 6
β’ ((π¦ β π΅ β§ π§ β π΅) β (π¦ β€ π§ β (π¦ < π§ β¨ π¦ = π§))) |
58 | 54, 56, 57 | syl2anc 585 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π¦ β€ π§ β (π¦ < π§ β¨ π¦ = π§))) |
59 | | potr 5602 |
. . . . . . . 8
β’ (( < Po π΅ β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ < π¦ β§ π¦ < π§) β π₯ < π§)) |
60 | 39, 59 | sylan 581 |
. . . . . . 7
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ < π¦ β§ π¦ < π§) β π₯ < π§)) |
61 | | simpll 766 |
. . . . . . . 8
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β πΎ β π) |
62 | 13, 1 | pltle 18286 |
. . . . . . . 8
β’ ((πΎ β π β§ π₯ β π΅ β§ π§ β π΅) β (π₯ < π§ β π₯ β€ π§)) |
63 | 61, 53, 56, 62 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ < π§ β π₯ β€ π§)) |
64 | 60, 63 | syld 47 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ < π¦ β§ π¦ < π§) β π₯ β€ π§)) |
65 | | breq1 5152 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ < π§ β π¦ < π§)) |
66 | 65 | biimpar 479 |
. . . . . . 7
β’ ((π₯ = π¦ β§ π¦ < π§) β π₯ < π§) |
67 | 66, 63 | syl5 34 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ = π¦ β§ π¦ < π§) β π₯ β€ π§)) |
68 | | breq2 5153 |
. . . . . . . 8
β’ (π¦ = π§ β (π₯ < π¦ β π₯ < π§)) |
69 | 68 | biimpac 480 |
. . . . . . 7
β’ ((π₯ < π¦ β§ π¦ = π§) β π₯ < π§) |
70 | 69, 63 | syl5 34 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ < π¦ β§ π¦ = π§) β π₯ β€ π§)) |
71 | 53, 33 | syldan 592 |
. . . . . . 7
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β π₯ β€ π₯) |
72 | | eqtr 2756 |
. . . . . . . 8
β’ ((π₯ = π¦ β§ π¦ = π§) β π₯ = π§) |
73 | 72 | breq2d 5161 |
. . . . . . 7
β’ ((π₯ = π¦ β§ π¦ = π§) β (π₯ β€ π₯ β π₯ β€ π§)) |
74 | 71, 73 | syl5ibcom 244 |
. . . . . 6
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ = π¦ β§ π¦ = π§) β π₯ β€ π§)) |
75 | 64, 67, 70, 74 | ccased 1038 |
. . . . 5
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (((π₯ < π¦ β¨ π₯ = π¦) β§ (π¦ < π§ β¨ π¦ = π§)) β π₯ β€ π§)) |
76 | 55, 58, 75 | syl2and 609 |
. . . 4
β’ (((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
77 | 23, 24, 25, 33, 52, 76 | isposd 18276 |
. . 3
β’ ((πΎ β π β§ ( < Po π΅ β§ ( I βΎ π΅) β β€ )) β πΎ β Poset) |
78 | 77 | ex 414 |
. 2
β’ (πΎ β π β (( < Po π΅ β§ ( I βΎ π΅) β β€ ) β πΎ β Poset)) |
79 | 22, 78 | impbid2 225 |
1
β’ (πΎ β π β (πΎ β Poset β ( < Po π΅ β§ ( I βΎ π΅) β β€ ))) |