Step | Hyp | Ref
| Expression |
1 | | simp2l 1200 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β π
β π΄) |
2 | | cdleme32.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | cdleme32.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | 2, 3 | atbase 38097 |
. . . 4
β’ (π
β π΄ β π
β π΅) |
5 | 1, 4 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β π
β π΅) |
6 | | cdleme32.o |
. . . 4
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) |
7 | | eqid 2733 |
. . . 4
β’
(β©π§
β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π)))) = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π)))) |
8 | 6, 7 | cdleme31so 39188 |
. . 3
β’ (π
β π΅ β β¦π
/ π₯β¦π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))))) |
9 | 5, 8 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β β¦π
/ π₯β¦π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))))) |
10 | | simp1 1137 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
11 | | simp3 1139 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β π β π) |
12 | | simp2 1138 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (π
β π΄ β§ Β¬ π
β€ π)) |
13 | | cdleme32.l |
. . . . 5
β’ β€ =
(leβπΎ) |
14 | | cdleme32.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
15 | | cdleme32.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
16 | | cdleme32.h |
. . . . 5
β’ π» = (LHypβπΎ) |
17 | | cdleme32.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
18 | | cdleme32.c |
. . . . 5
β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
19 | | cdleme32.d |
. . . . 5
β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
20 | | cdleme32.e |
. . . . 5
β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) |
21 | | cdleme32.i |
. . . . 5
β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) |
22 | | cdleme32.n |
. . . . 5
β’ π = if(π β€ (π β¨ π), πΌ, πΆ) |
23 | 2, 13, 14, 15, 3, 16, 17, 18, 19, 20, 21, 22 | cdleme32snb 39245 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π))) β β¦π
/ π β¦π β π΅) |
24 | 10, 11, 12, 23 | syl12anc 836 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β β¦π
/ π β¦π β π΅) |
25 | | nfv 1918 |
. . . . . . . . 9
β’
β²π Β¬ π
β€ π |
26 | | nfcsb1v 3917 |
. . . . . . . . . 10
β’
β²π β¦π
/ π β¦π |
27 | 26 | nfeq2 2921 |
. . . . . . . . 9
β’
β²π π§ = β¦π
/ π β¦π |
28 | 25, 27 | nfim 1900 |
. . . . . . . 8
β’
β²π (Β¬ π
β€ π β π§ = β¦π
/ π β¦π) |
29 | | breq1 5150 |
. . . . . . . . . . 11
β’ (π = π
β (π β€ π β π
β€ π)) |
30 | 29 | notbid 318 |
. . . . . . . . . 10
β’ (π = π
β (Β¬ π β€ π β Β¬ π
β€ π)) |
31 | | csbeq1a 3906 |
. . . . . . . . . . 11
β’ (π = π
β π = β¦π
/ π β¦π) |
32 | 31 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π = π
β (π§ = π β π§ = β¦π
/ π β¦π)) |
33 | 30, 32 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π
β ((Β¬ π β€ π β π§ = π) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
34 | 33 | ax-gen 1798 |
. . . . . . . 8
β’
βπ (π = π
β ((Β¬ π β€ π β π§ = π) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
35 | | ceqsralt 3506 |
. . . . . . . 8
β’
((β²π (Β¬
π
β€ π β π§ = β¦π
/ π β¦π) β§ βπ (π = π
β ((Β¬ π β€ π β π§ = π) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) β§ π
β π΄) β (βπ β π΄ (π = π
β (Β¬ π β€ π β π§ = π)) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
36 | 28, 34, 35 | mp3an12 1452 |
. . . . . . 7
β’ (π
β π΄ β (βπ β π΄ (π = π
β (Β¬ π β€ π β π§ = π)) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
37 | 36 | adantr 482 |
. . . . . 6
β’ ((π
β π΄ β§ Β¬ π
β€ π) β (βπ β π΄ (π = π
β (Β¬ π β€ π β π§ = π)) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
38 | 37 | 3ad2ant2 1135 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (βπ β π΄ (π = π
β (Β¬ π β€ π β π§ = π)) β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
39 | | simp11 1204 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (πΎ β HL β§ π β π»)) |
40 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0.βπΎ) =
(0.βπΎ) |
41 | 13, 15, 40, 3, 16 | lhpmat 38839 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π
β§ π) = (0.βπΎ)) |
42 | 39, 12, 41 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (π
β§ π) = (0.βπΎ)) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β§ π) = (0.βπΎ)) |
44 | 43 | oveq2d 7420 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β§ π)) = (π β¨ (0.βπΎ))) |
45 | | simp11l 1285 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β πΎ β HL) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
47 | | hlol 38169 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β πΎ β OL) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β OL) |
49 | 2, 3 | atbase 38097 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β π΅) |
50 | 49 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΅) |
51 | 2, 14, 40 | olj01 38033 |
. . . . . . . . . . . . 13
β’ ((πΎ β OL β§ π β π΅) β (π β¨ (0.βπΎ)) = π ) |
52 | 48, 50, 51 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (0.βπΎ)) = π ) |
53 | 44, 52 | eqtrd 2773 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β§ π)) = π ) |
54 | 53 | eqeq1d 2735 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (π
β§ π)) = π
β π = π
)) |
55 | 43 | oveq2d 7420 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β§ π)) = (π β¨ (0.βπΎ))) |
56 | | simpl11 1249 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
57 | | simpl12 1250 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
58 | | simpl13 1251 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
59 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
60 | | simpl3 1194 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π) |
61 | 2, 13, 14, 15, 3, 16, 17, 18, 19, 20, 21, 22 | cdleme27cl 39175 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π)) β π β π΅) |
62 | 56, 57, 58, 59, 60, 61 | syl122anc 1380 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΅) |
63 | 2, 14, 40 | olj01 38033 |
. . . . . . . . . . . . 13
β’ ((πΎ β OL β§ π β π΅) β (π β¨ (0.βπΎ)) = π) |
64 | 48, 62, 63 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (0.βπΎ)) = π) |
65 | 55, 64 | eqtrd 2773 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β§ π)) = π) |
66 | 65 | eqeq2d 2744 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π§ = (π β¨ (π
β§ π)) β π§ = π)) |
67 | 54, 66 | imbi12d 345 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (π
β§ π)) = π
β π§ = (π β¨ (π
β§ π))) β (π = π
β π§ = π))) |
68 | 67 | expr 458 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ π β π΄) β (Β¬ π β€ π β (((π β¨ (π
β§ π)) = π
β π§ = (π β¨ (π
β§ π))) β (π = π
β π§ = π)))) |
69 | 68 | pm5.74d 273 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ π β π΄) β ((Β¬ π β€ π β ((π β¨ (π
β§ π)) = π
β π§ = (π β¨ (π
β§ π)))) β (Β¬ π β€ π β (π = π
β π§ = π)))) |
70 | | impexp 452 |
. . . . . . 7
β’ (((Β¬
π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β (Β¬ π β€ π β ((π β¨ (π
β§ π)) = π
β π§ = (π β¨ (π
β§ π))))) |
71 | | bi2.04 389 |
. . . . . . 7
β’ ((π = π
β (Β¬ π β€ π β π§ = π)) β (Β¬ π β€ π β (π = π
β π§ = π))) |
72 | 69, 70, 71 | 3bitr4g 314 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ π β π΄) β (((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β (π = π
β (Β¬ π β€ π β π§ = π)))) |
73 | 72 | ralbidva 3176 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β βπ β π΄ (π = π
β (Β¬ π β€ π β π§ = π)))) |
74 | | simp2r 1201 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β Β¬ π
β€ π) |
75 | | biimt 361 |
. . . . . 6
β’ (Β¬
π
β€ π β (π§ = β¦π
/ π β¦π β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
76 | 74, 75 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (π§ = β¦π
/ π β¦π β (Β¬ π
β€ π β π§ = β¦π
/ π β¦π))) |
77 | 38, 73, 76 | 3bitr4d 311 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β π§ = β¦π
/ π β¦π)) |
78 | 77 | adantr 482 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β§ π§ β π΅) β (βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π))) β π§ = β¦π
/ π β¦π)) |
79 | 24, 78 | riota5 7390 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π
β§ π)) = π
) β π§ = (π β¨ (π
β§ π)))) = β¦π
/ π β¦π) |
80 | 9, 79 | eqtrd 2773 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ π β π) β β¦π
/ π₯β¦π = β¦π
/ π β¦π) |