Step | Hyp | Ref
| Expression |
1 | | simprrl 780 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β βπ¦ β π π€ β€ π¦) |
2 | | breq1 5152 |
. . . . . . . . 9
β’ (π§ = π€ β (π§ β€ π¦ β π€ β€ π¦)) |
3 | 2 | ralbidv 3178 |
. . . . . . . 8
β’ (π§ = π€ β (βπ¦ β π π§ β€ π¦ β βπ¦ β π π€ β€ π¦)) |
4 | | breq1 5152 |
. . . . . . . 8
β’ (π§ = π€ β (π§ β€ π₯ β π€ β€ π₯)) |
5 | 3, 4 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π€ β ((βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β (βπ¦ β π π€ β€ π¦ β π€ β€ π₯))) |
6 | | simprlr 779 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) |
7 | | simplrr 777 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β π€ β π΅) |
8 | 5, 6, 7 | rspcdva 3614 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β (βπ¦ β π π€ β€ π¦ β π€ β€ π₯)) |
9 | 1, 8 | mpd 15 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β π€ β€ π₯) |
10 | | simprll 778 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β βπ¦ β π π₯ β€ π¦) |
11 | | breq1 5152 |
. . . . . . . . 9
β’ (π§ = π₯ β (π§ β€ π¦ β π₯ β€ π¦)) |
12 | 11 | ralbidv 3178 |
. . . . . . . 8
β’ (π§ = π₯ β (βπ¦ β π π§ β€ π¦ β βπ¦ β π π₯ β€ π¦)) |
13 | | breq1 5152 |
. . . . . . . 8
β’ (π§ = π₯ β (π§ β€ π€ β π₯ β€ π€)) |
14 | 12, 13 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π₯ β ((βπ¦ β π π§ β€ π¦ β π§ β€ π€) β (βπ¦ β π π₯ β€ π¦ β π₯ β€ π€))) |
15 | | simprrr 781 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)) |
16 | | simplrl 776 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β π₯ β π΅) |
17 | 14, 15, 16 | rspcdva 3614 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β (βπ¦ β π π₯ β€ π¦ β π₯ β€ π€)) |
18 | 10, 17 | mpd 15 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β π₯ β€ π€) |
19 | | ancom 462 |
. . . . . . . 8
β’ ((π€ β€ π₯ β§ π₯ β€ π€) β (π₯ β€ π€ β§ π€ β€ π₯)) |
20 | | poslubmo.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
21 | | poslubmo.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
22 | 20, 21 | posasymb 18272 |
. . . . . . . 8
β’ ((πΎ β Poset β§ π₯ β π΅ β§ π€ β π΅) β ((π₯ β€ π€ β§ π€ β€ π₯) β π₯ = π€)) |
23 | 19, 22 | bitrid 283 |
. . . . . . 7
β’ ((πΎ β Poset β§ π₯ β π΅ β§ π€ β π΅) β ((π€ β€ π₯ β§ π₯ β€ π€) β π₯ = π€)) |
24 | 23 | 3expb 1121 |
. . . . . 6
β’ ((πΎ β Poset β§ (π₯ β π΅ β§ π€ β π΅)) β ((π€ β€ π₯ β§ π₯ β€ π€) β π₯ = π€)) |
25 | 24 | ad4ant13 750 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β ((π€ β€ π₯ β§ π₯ β€ π€) β π₯ = π€)) |
26 | 9, 18, 25 | mpbi2and 711 |
. . . 4
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) β π₯ = π€) |
27 | 26 | ex 414 |
. . 3
β’ (((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β (((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€))) β π₯ = π€)) |
28 | 27 | ralrimivva 3201 |
. 2
β’ ((πΎ β Poset β§ π β π΅) β βπ₯ β π΅ βπ€ β π΅ (((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€))) β π₯ = π€)) |
29 | | breq1 5152 |
. . . . 5
β’ (π₯ = π€ β (π₯ β€ π¦ β π€ β€ π¦)) |
30 | 29 | ralbidv 3178 |
. . . 4
β’ (π₯ = π€ β (βπ¦ β π π₯ β€ π¦ β βπ¦ β π π€ β€ π¦)) |
31 | | breq2 5153 |
. . . . . 6
β’ (π₯ = π€ β (π§ β€ π₯ β π§ β€ π€)) |
32 | 31 | imbi2d 341 |
. . . . 5
β’ (π₯ = π€ β ((βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β (βπ¦ β π π§ β€ π¦ β π§ β€ π€))) |
33 | 32 | ralbidv 3178 |
. . . 4
β’ (π₯ = π€ β (βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€))) |
34 | 30, 33 | anbi12d 632 |
. . 3
β’ (π₯ = π€ β ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€)))) |
35 | 34 | rmo4 3727 |
. 2
β’
(β*π₯ β
π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β βπ₯ β π΅ βπ€ β π΅ (((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β§ (βπ¦ β π π€ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π€))) β π₯ = π€)) |
36 | 28, 35 | sylibr 233 |
1
β’ ((πΎ β Poset β§ π β π΅) β β*π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |