Step | Hyp | Ref
| Expression |
1 | | dihglblem.t |
. . 3
β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} |
2 | 1 | a1i 11 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)}) |
3 | | simprr 772 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β π β β
) |
4 | | n0 4310 |
. . . 4
β’ (π β β
β
βπ§ π§ β π) |
5 | 3, 4 | sylib 217 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β βπ§ π§ β π) |
6 | | hllat 37875 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
7 | 6 | ad3antrrr 729 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β πΎ β Lat) |
8 | | simplrl 776 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β π β π΅) |
9 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β π§ β π) |
10 | 8, 9 | sseldd 3949 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β π§ β π΅) |
11 | | dihglblem.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
12 | | dihglblem.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
13 | 11, 12 | lhpbase 38511 |
. . . . . . 7
β’ (π β π» β π β π΅) |
14 | 13 | ad3antlr 730 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β π β π΅) |
15 | | dihglblem.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
16 | 11, 15 | latmcl 18337 |
. . . . . 6
β’ ((πΎ β Lat β§ π§ β π΅ β§ π β π΅) β (π§ β§ π) β π΅) |
17 | 7, 10, 14, 16 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β (π§ β§ π) β π΅) |
18 | | eqidd 2734 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β (π§ β§ π) = (π§ β§ π)) |
19 | | oveq1 7368 |
. . . . . . 7
β’ (π£ = π§ β (π£ β§ π) = (π§ β§ π)) |
20 | 19 | rspceeqv 3599 |
. . . . . 6
β’ ((π§ β π β§ (π§ β§ π) = (π§ β§ π)) β βπ£ β π (π§ β§ π) = (π£ β§ π)) |
21 | 9, 18, 20 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β βπ£ β π (π§ β§ π) = (π£ β§ π)) |
22 | | ovex 7394 |
. . . . . 6
β’ (π§ β§ π) β V |
23 | | eleq1 2822 |
. . . . . . 7
β’ (π€ = (π§ β§ π) β (π€ β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β (π§ β§ π) β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)})) |
24 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π’ = (π§ β§ π) β (π’ = (π£ β§ π) β (π§ β§ π) = (π£ β§ π))) |
25 | 24 | rexbidv 3172 |
. . . . . . . 8
β’ (π’ = (π§ β§ π) β (βπ£ β π π’ = (π£ β§ π) β βπ£ β π (π§ β§ π) = (π£ β§ π))) |
26 | 25 | elrab 3649 |
. . . . . . 7
β’ ((π§ β§ π) β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β ((π§ β§ π) β π΅ β§ βπ£ β π (π§ β§ π) = (π£ β§ π))) |
27 | 23, 26 | bitrdi 287 |
. . . . . 6
β’ (π€ = (π§ β§ π) β (π€ β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β ((π§ β§ π) β π΅ β§ βπ£ β π (π§ β§ π) = (π£ β§ π)))) |
28 | 22, 27 | spcev 3567 |
. . . . 5
β’ (((π§ β§ π) β π΅ β§ βπ£ β π (π§ β§ π) = (π£ β§ π)) β βπ€ π€ β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)}) |
29 | 17, 21, 28 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β βπ€ π€ β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)}) |
30 | | n0 4310 |
. . . 4
β’ ({π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β β
β βπ€ π€ β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)}) |
31 | 29, 30 | sylibr 233 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β§ π§ β π) β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β β
) |
32 | 5, 31 | exlimddv 1939 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β β
) |
33 | 2, 32 | eqnetrd 3008 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β
)) β π β β
) |