Step | Hyp | Ref
| Expression |
1 | | pospropd.xy |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) |
2 | 1 | ralrimivva 3198 |
. . . . . . . . . 10
β’ (π β βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) |
3 | | simp1 1134 |
. . . . . . . . . . . . 13
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β π β π΅) |
4 | 3, 3 | jca 510 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
5 | | breq1 5150 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯(leβπΎ)π¦ β π(leβπΎ)π¦)) |
6 | | breq1 5150 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯(leβπΏ)π¦ β π(leβπΏ)π¦)) |
7 | 5, 6 | bibi12d 344 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦) β (π(leβπΎ)π¦ β π(leβπΏ)π¦))) |
8 | | breq2 5151 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π(leβπΎ)π¦ β π(leβπΎ)π)) |
9 | | breq2 5151 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π(leβπΏ)π¦ β π(leβπΏ)π)) |
10 | 8, 9 | bibi12d 344 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((π(leβπΎ)π¦ β π(leβπΏ)π¦) β (π(leβπΎ)π β π(leβπΏ)π))) |
11 | 7, 10 | rspc2va 3622 |
. . . . . . . . . . . 12
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
12 | 4, 11 | sylan 578 |
. . . . . . . . . . 11
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
13 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΎ)π¦ β π(leβπΎ)π)) |
14 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΏ)π¦ β π(leβπΏ)π)) |
15 | 13, 14 | bibi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((π(leβπΎ)π¦ β π(leβπΏ)π¦) β (π(leβπΎ)π β π(leβπΏ)π))) |
16 | 7, 15 | rspc2va 3622 |
. . . . . . . . . . . . . 14
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
17 | 16 | 3adantl3 1166 |
. . . . . . . . . . . . 13
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
18 | | 3simpb 1147 |
. . . . . . . . . . . . . . 15
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
19 | 18 | 3comr 1123 |
. . . . . . . . . . . . . 14
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
20 | | breq1 5150 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯(leβπΎ)π¦ β π(leβπΎ)π¦)) |
21 | | breq1 5150 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯(leβπΏ)π¦ β π(leβπΏ)π¦)) |
22 | 20, 21 | bibi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦) β (π(leβπΎ)π¦ β π(leβπΏ)π¦))) |
23 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΎ)π¦ β π(leβπΎ)π)) |
24 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΏ)π¦ β π(leβπΏ)π)) |
25 | 23, 24 | bibi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((π(leβπΎ)π¦ β π(leβπΏ)π¦) β (π(leβπΎ)π β π(leβπΏ)π))) |
26 | 22, 25 | rspc2va 3622 |
. . . . . . . . . . . . . 14
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
27 | 19, 26 | sylan 578 |
. . . . . . . . . . . . 13
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
28 | 17, 27 | anbi12d 629 |
. . . . . . . . . . . 12
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π(leβπΏ)π β§ π(leβπΏ)π))) |
29 | 28 | imbi1d 340 |
. . . . . . . . . . 11
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π))) |
30 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΎ)π¦ β π(leβπΎ)π)) |
31 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π(leβπΏ)π¦ β π(leβπΏ)π)) |
32 | 30, 31 | bibi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((π(leβπΎ)π¦ β π(leβπΏ)π¦) β (π(leβπΎ)π β π(leβπΏ)π))) |
33 | 22, 32 | rspc2va 3622 |
. . . . . . . . . . . . . 14
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
34 | 33 | 3adantl1 1164 |
. . . . . . . . . . . . 13
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
35 | 17, 34 | anbi12d 629 |
. . . . . . . . . . . 12
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π(leβπΏ)π β§ π(leβπΏ)π))) |
36 | | 3simpb 1147 |
. . . . . . . . . . . . 13
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
37 | | breq2 5151 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π(leβπΎ)π¦ β π(leβπΎ)π)) |
38 | | breq2 5151 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π(leβπΏ)π¦ β π(leβπΏ)π)) |
39 | 37, 38 | bibi12d 344 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β ((π(leβπΎ)π¦ β π(leβπΏ)π¦) β (π(leβπΎ)π β π(leβπΏ)π))) |
40 | 7, 39 | rspc2va 3622 |
. . . . . . . . . . . . 13
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
41 | 36, 40 | sylan 578 |
. . . . . . . . . . . 12
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (π(leβπΎ)π β π(leβπΏ)π)) |
42 | 35, 41 | imbi12d 343 |
. . . . . . . . . . 11
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β (((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π) β ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π))) |
43 | 12, 29, 42 | 3anbi123d 1434 |
. . . . . . . . . 10
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯(leβπΎ)π¦ β π₯(leβπΏ)π¦)) β ((π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
44 | 2, 43 | sylan2 591 |
. . . . . . . . 9
β’ (((π β π΅ β§ π β π΅ β§ π β π΅) β§ π) β ((π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
45 | 44 | ancoms 457 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
46 | 45 | 3exp2 1352 |
. . . . . . 7
β’ (π β (π β π΅ β (π β π΅ β (π β π΅ β ((π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π))))))) |
47 | 46 | imp42 425 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π β π΅) β ((π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
48 | 47 | ralbidva 3173 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
49 | 48 | 2ralbidva 3214 |
. . . 4
β’ (π β (βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
50 | | pospropd.kb |
. . . . 5
β’ (π β π΅ = (BaseβπΎ)) |
51 | | raleq 3320 |
. . . . . . 7
β’ (π΅ = (BaseβπΎ) β (βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)))) |
52 | 51 | raleqbi1dv 3331 |
. . . . . 6
β’ (π΅ = (BaseβπΎ) β (βπ β π΅ βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)))) |
53 | 52 | raleqbi1dv 3331 |
. . . . 5
β’ (π΅ = (BaseβπΎ) β (βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)))) |
54 | 50, 53 | syl 17 |
. . . 4
β’ (π β (βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)))) |
55 | | pospropd.lb |
. . . . 5
β’ (π β π΅ = (BaseβπΏ)) |
56 | | raleq 3320 |
. . . . . . 7
β’ (π΅ = (BaseβπΏ) β (βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)) β βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
57 | 56 | raleqbi1dv 3331 |
. . . . . 6
β’ (π΅ = (BaseβπΏ) β (βπ β π΅ βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)) β βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
58 | 57 | raleqbi1dv 3331 |
. . . . 5
β’ (π΅ = (BaseβπΏ) β (βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)) β βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
59 | 55, 58 | syl 17 |
. . . 4
β’ (π β (βπ β π΅ βπ β π΅ βπ β π΅ (π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)) β βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
60 | 49, 54, 59 | 3bitr3d 308 |
. . 3
β’ (π β (βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
61 | | pospropd.kv |
. . . . 5
β’ (π β πΎ β π) |
62 | 61 | elexd 3493 |
. . . 4
β’ (π β πΎ β V) |
63 | 62 | biantrurd 531 |
. . 3
β’ (π β (βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)) β (πΎ β V β§ βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π))))) |
64 | | pospropd.lv |
. . . . 5
β’ (π β πΏ β π) |
65 | 64 | elexd 3493 |
. . . 4
β’ (π β πΏ β V) |
66 | 65 | biantrurd 531 |
. . 3
β’ (π β (βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)) β (πΏ β V β§ βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π))))) |
67 | 60, 63, 66 | 3bitr3d 308 |
. 2
β’ (π β ((πΎ β V β§ βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π))) β (πΏ β V β§ βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π))))) |
68 | | eqid 2730 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
69 | | eqid 2730 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
70 | 68, 69 | ispos 18271 |
. 2
β’ (πΎ β Poset β (πΎ β V β§ βπ β (BaseβπΎ)βπ β (BaseβπΎ)βπ β (BaseβπΎ)(π(leβπΎ)π β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π) β§ ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)π)))) |
71 | | eqid 2730 |
. . 3
β’
(BaseβπΏ) =
(BaseβπΏ) |
72 | | eqid 2730 |
. . 3
β’
(leβπΏ) =
(leβπΏ) |
73 | 71, 72 | ispos 18271 |
. 2
β’ (πΏ β Poset β (πΏ β V β§ βπ β (BaseβπΏ)βπ β (BaseβπΏ)βπ β (BaseβπΏ)(π(leβπΏ)π β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π = π) β§ ((π(leβπΏ)π β§ π(leβπΏ)π) β π(leβπΏ)π)))) |
74 | 67, 70, 73 | 3bitr4g 313 |
1
β’ (π β (πΎ β Poset β πΏ β Poset)) |