Step | Hyp | Ref
| Expression |
1 | | cdleme26.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | cdleme26.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | cdleme26.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
4 | | cdleme26.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
5 | | cdleme26.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
6 | | cdleme26.h |
. . . . 5
β’ π» = (LHypβπΎ) |
7 | | cdleme27.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
8 | | cdleme27.f |
. . . . 5
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
9 | | cdleme27.z |
. . . . 5
β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
10 | | cdleme27.n |
. . . . 5
β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
11 | | cdleme27.d |
. . . . 5
β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
12 | | cdleme27.c |
. . . . 5
β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) |
13 | | cdleme27.g |
. . . . 5
β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
14 | | cdleme27.o |
. . . . 5
β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) |
15 | | cdleme27.e |
. . . . 5
β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
16 | | cdleme27.y |
. . . . 5
β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | cdleme27b 38860 |
. . . 4
β’ (π = π‘ β πΆ = π) |
18 | 17 | adantl 483 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π = π‘) β πΆ = π) |
19 | | simp11l 1285 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β πΎ β HL) |
20 | 19 | hllatd 37855 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β πΎ β Lat) |
21 | | simp11r 1286 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β π») |
22 | | simp21 1207 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β (π β π΄ β§ Β¬ π β€ π)) |
23 | | simp22 1208 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β (π β π΄ β§ Β¬ π β€ π)) |
24 | | simp23 1209 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β (π‘ β π΄ β§ Β¬ π‘ β€ π)) |
25 | | simp12 1205 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β π) |
26 | 1, 2, 3, 4, 5, 6, 7, 13, 9, 14, 15, 16 | cdleme27cl 38858 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ π β π)) β π β π΅) |
27 | 19, 21, 22, 23, 24, 25, 26 | syl222anc 1387 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β π΅) |
28 | | simp3rl 1247 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β π΄) |
29 | 1, 5 | atbase 37780 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β π΅) |
31 | 1, 2, 3 | latlej1 18344 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) |
32 | 20, 27, 30, 31 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β π β€ (π β¨ π)) |
33 | 32 | adantr 482 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π = π‘) β π β€ (π β¨ π)) |
34 | 18, 33 | eqbrtrd 5132 |
. 2
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π = π‘) β πΆ β€ (π β¨ π)) |
35 | | simpl11 1249 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (πΎ β HL β§ π β π»)) |
36 | | simpl12 1250 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β π β π) |
37 | | simpl13 1251 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π β π΄ β§ Β¬ π β€ π)) |
38 | | simpl21 1252 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π β π΄ β§ Β¬ π β€ π)) |
39 | | simpl22 1253 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π β π΄ β§ Β¬ π β€ π)) |
40 | | simpl23 1254 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π‘ β π΄ β§ Β¬ π‘ β€ π)) |
41 | | simpr 486 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β π β π‘) |
42 | | simpl3l 1229 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β π β€ (π‘ β¨ π)) |
43 | 41, 42 | jca 513 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π β π‘ β§ π β€ (π‘ β¨ π))) |
44 | | simpl3r 1230 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β (π β π΄ β§ π β€ π)) |
45 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | cdleme27a 38859 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β π‘ β§ π β€ (π‘ β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΆ β€ (π β¨ π)) |
46 | 35, 36, 37, 38, 39, 40, 43, 44, 45 | syl332anc 1402 |
. 2
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β§ π β π‘) β πΆ β€ (π β¨ π)) |
47 | 34, 46 | pm2.61dane 3033 |
1
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β πΆ β€ (π β¨ π)) |