Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
2 | | simp12 1205 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β π β π) |
3 | | simp2l 1200 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β π β π΄) |
4 | | simp3ll 1245 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β Β¬ π β€ π) |
5 | 3, 4 | jca 513 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (π β π΄ β§ Β¬ π β€ π)) |
6 | | simp2r 1201 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β π‘ β π΄) |
7 | | simp3rl 1247 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β Β¬ π‘ β€ π) |
8 | 6, 7 | jca 513 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (π‘ β π΄ β§ Β¬ π‘ β€ π)) |
9 | | simp3lr 1246 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (π β¨ (π β§ π)) = π) |
10 | | simp3rr 1248 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (π‘ β¨ (π β§ π)) = π) |
11 | | simp13 1206 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (π β π΅ β§ Β¬ π β€ π)) |
12 | | cdleme26.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
13 | | cdleme26.l |
. . . . 5
β’ β€ =
(leβπΎ) |
14 | | cdleme26.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
15 | | cdleme26.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
16 | | cdleme26.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
17 | | cdleme26.h |
. . . . 5
β’ π» = (LHypβπΎ) |
18 | | cdleme27.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
19 | | cdleme27.f |
. . . . 5
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
20 | | cdleme27.z |
. . . . 5
β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
21 | | cdleme27.n |
. . . . 5
β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
22 | | cdleme27.d |
. . . . 5
β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
23 | | cdleme27.c |
. . . . 5
β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) |
24 | | cdleme27.g |
. . . . 5
β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
25 | | cdleme27.o |
. . . . 5
β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) |
26 | | cdleme27.e |
. . . . 5
β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
27 | | cdleme27.y |
. . . . 5
β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) |
28 | 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 | cdleme28c 38864 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) |
29 | 1, 2, 5, 8, 9, 10,
11, 28 | syl133anc 1394 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) |
30 | 29 | 3exp 1120 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β ((π β π΄ β§ π‘ β π΄) β (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))))) |
31 | 30 | ralrimivv 3196 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π)))) |