Step | Hyp | Ref
| Expression |
1 | | simprrl 779 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β βπ¦ β π π¦ β€ π€) |
2 | | breq2 5152 |
. . . . . . . . 9
β’ (π§ = π€ β (π¦ β€ π§ β π¦ β€ π€)) |
3 | 2 | ralbidv 3177 |
. . . . . . . 8
β’ (π§ = π€ β (βπ¦ β π π¦ β€ π§ β βπ¦ β π π¦ β€ π€)) |
4 | | breq2 5152 |
. . . . . . . 8
β’ (π§ = π€ β (π₯ β€ π§ β π₯ β€ π€)) |
5 | 3, 4 | imbi12d 344 |
. . . . . . 7
β’ (π§ = π€ β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦ β€ π€ β π₯ β€ π€))) |
6 | | simprlr 778 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) |
7 | | simplrr 776 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β π€ β π΅) |
8 | 5, 6, 7 | rspcdva 3613 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β (βπ¦ β π π¦ β€ π€ β π₯ β€ π€)) |
9 | 1, 8 | mpd 15 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β π₯ β€ π€) |
10 | | simprll 777 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β βπ¦ β π π¦ β€ π₯) |
11 | | breq2 5152 |
. . . . . . . . 9
β’ (π§ = π₯ β (π¦ β€ π§ β π¦ β€ π₯)) |
12 | 11 | ralbidv 3177 |
. . . . . . . 8
β’ (π§ = π₯ β (βπ¦ β π π¦ β€ π§ β βπ¦ β π π¦ β€ π₯)) |
13 | | breq2 5152 |
. . . . . . . 8
β’ (π§ = π₯ β (π€ β€ π§ β π€ β€ π₯)) |
14 | 12, 13 | imbi12d 344 |
. . . . . . 7
β’ (π§ = π₯ β ((βπ¦ β π π¦ β€ π§ β π€ β€ π§) β (βπ¦ β π π¦ β€ π₯ β π€ β€ π₯))) |
15 | | simprrr 780 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)) |
16 | | simplrl 775 |
. . . . . . 7
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β π₯ β π΅) |
17 | 14, 15, 16 | rspcdva 3613 |
. . . . . 6
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β (βπ¦ β π π¦ β€ π₯ β π€ β€ π₯)) |
18 | 10, 17 | mpd 15 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β π€ β€ π₯) |
19 | | poslubmo.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
20 | | poslubmo.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
21 | 19, 20 | posasymb 18271 |
. . . . . . 7
β’ ((πΎ β Poset β§ π₯ β π΅ β§ π€ β π΅) β ((π₯ β€ π€ β§ π€ β€ π₯) β π₯ = π€)) |
22 | 21 | 3expb 1120 |
. . . . . 6
β’ ((πΎ β Poset β§ (π₯ β π΅ β§ π€ β π΅)) β ((π₯ β€ π€ β§ π€ β€ π₯) β π₯ = π€)) |
23 | 22 | ad4ant13 749 |
. . . . 5
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β ((π₯ β€ π€ β§ π€ β€ π₯) β π₯ = π€)) |
24 | 9, 18, 23 | mpbi2and 710 |
. . . 4
β’ ((((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β§ ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) β π₯ = π€) |
25 | 24 | ex 413 |
. . 3
β’ (((πΎ β Poset β§ π β π΅) β§ (π₯ β π΅ β§ π€ β π΅)) β (((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§))) β π₯ = π€)) |
26 | 25 | ralrimivva 3200 |
. 2
β’ ((πΎ β Poset β§ π β π΅) β βπ₯ β π΅ βπ€ β π΅ (((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§))) β π₯ = π€)) |
27 | | breq2 5152 |
. . . . 5
β’ (π₯ = π€ β (π¦ β€ π₯ β π¦ β€ π€)) |
28 | 27 | ralbidv 3177 |
. . . 4
β’ (π₯ = π€ β (βπ¦ β π π¦ β€ π₯ β βπ¦ β π π¦ β€ π€)) |
29 | | breq1 5151 |
. . . . . 6
β’ (π₯ = π€ β (π₯ β€ π§ β π€ β€ π§)) |
30 | 29 | imbi2d 340 |
. . . . 5
β’ (π₯ = π€ β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦ β€ π§ β π€ β€ π§))) |
31 | 30 | ralbidv 3177 |
. . . 4
β’ (π₯ = π€ β (βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§))) |
32 | 28, 31 | anbi12d 631 |
. . 3
β’ (π₯ = π€ β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§)))) |
33 | 32 | rmo4 3726 |
. 2
β’
(β*π₯ β
π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β βπ₯ β π΅ βπ€ β π΅ (((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β§ (βπ¦ β π π¦ β€ π€ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π€ β€ π§))) β π₯ = π€)) |
34 | 26, 33 | sylibr 233 |
1
β’ ((πΎ β Poset β§ π β π΅) β β*π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |