Step | Hyp | Ref
| Expression |
1 | | cdlemf.l |
. . 3
β’ β€ =
(leβπΎ) |
2 | | eqid 2733 |
. . 3
β’
(joinβπΎ) =
(joinβπΎ) |
3 | | cdlemf.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
4 | | cdlemf.h |
. . 3
β’ π» = (LHypβπΎ) |
5 | | eqid 2733 |
. . 3
β’
(meetβπΎ) =
(meetβπΎ) |
6 | 1, 2, 3, 4, 5 | cdlemf2 39075 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) |
7 | | simp1l 1198 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β (πΎ β HL β§ π β π»)) |
8 | | simp2l 1200 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β π β π΄) |
9 | | simp3ll 1245 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β Β¬ π β€ π) |
10 | | simp2r 1201 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β π β π΄) |
11 | | simp3lr 1246 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β Β¬ π β€ π) |
12 | | cdlemf.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
13 | 1, 3, 4, 12 | cdleme50ex 39072 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π (πβπ) = π) |
14 | 7, 8, 9, 10, 11, 13 | syl122anc 1380 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β βπ β π (πβπ) = π) |
15 | | simp3r 1203 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β (πβπ) = π) |
16 | 15 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β (π(joinβπΎ)(πβπ)) = (π(joinβπΎ)π)) |
17 | 16 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β ((π(joinβπΎ)(πβπ))(meetβπΎ)π) = ((π(joinβπΎ)π)(meetβπΎ)π)) |
18 | | simp11 1204 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β (πΎ β HL β§ π β π»)) |
19 | | simp3l 1202 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β π β π) |
20 | | simp13l 1289 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β π β π΄) |
21 | | simp2ll 1241 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β Β¬ π β€ π) |
22 | | cdlemf.r |
. . . . . . . . . . . . 13
β’ π
= ((trLβπΎ)βπ) |
23 | 1, 2, 5, 3, 4, 12,
22 | trlval2 38676 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπ) = ((π(joinβπΎ)(πβπ))(meetβπΎ)π)) |
24 | 18, 19, 20, 21, 23 | syl112anc 1375 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β (π
βπ) = ((π(joinβπΎ)(πβπ))(meetβπΎ)π)) |
25 | | simp2r 1201 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β π = ((π(joinβπΎ)π)(meetβπΎ)π)) |
26 | 17, 24, 25 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β§ (π β π β§ (πβπ) = π)) β (π
βπ) = π) |
27 | 26 | 3exp 1120 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β π΄)) β (((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β ((π β π β§ (πβπ) = π) β (π
βπ) = π))) |
28 | 27 | 3expia 1122 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ π β π΄) β (((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β ((π β π β§ (πβπ) = π) β (π
βπ) = π)))) |
29 | 28 | 3imp 1112 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β ((π β π β§ (πβπ) = π) β (π
βπ) = π)) |
30 | 29 | expd 417 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β (π β π β ((πβπ) = π β (π
βπ) = π))) |
31 | 30 | reximdvai 3159 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β (βπ β π (πβπ) = π β βπ β π (π
βπ) = π)) |
32 | 14, 31 | mpd 15 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π))) β βπ β π (π
βπ) = π) |
33 | 32 | 3exp 1120 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ π β π΄) β (((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β βπ β π (π
βπ) = π))) |
34 | 33 | rexlimdvv 3201 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β (βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π(joinβπΎ)π)(meetβπΎ)π)) β βπ β π (π
βπ) = π)) |
35 | 6, 34 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π (π
βπ) = π) |