Step | Hyp | Ref
| Expression |
1 | | 3dim0.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
2 | | 3dim0.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | 3dim0.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
4 | 1, 2, 3 | 3dim1 37959 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
5 | 4 | 3adant2 1132 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
6 | | simpl21 1252 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β π’ β π΄) |
7 | | simpl22 1253 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β π£ β π΄) |
8 | | simp31 1210 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π β π’) |
9 | 8 | necomd 3000 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π’ β π) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β π’ β π) |
11 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β¨ π) = (π β¨ π)) |
12 | | simp11 1204 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β πΎ β HL) |
13 | | simp13 1206 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π β π΄) |
14 | 1, 3 | hlatjidm 37860 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π β¨ π) = π) |
16 | 11, 15 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (π β¨ π) = π) |
17 | 16 | breq2d 5122 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (π’ β€ (π β¨ π) β π’ β€ π)) |
18 | 17 | notbid 318 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (Β¬ π’ β€ (π β¨ π) β Β¬ π’ β€ π)) |
19 | | hlatl 37851 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β πΎ β AtLat) |
20 | 12, 19 | syl 17 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β πΎ β AtLat) |
21 | | simp21 1207 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π’ β π΄) |
22 | 2, 3 | atncmp 37803 |
. . . . . . . . . . . . 13
β’ ((πΎ β AtLat β§ π’ β π΄ β§ π β π΄) β (Β¬ π’ β€ π β π’ β π)) |
23 | 20, 21, 13, 22 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (Β¬ π’ β€ π β π’ β π)) |
24 | 23 | adantr 482 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (Β¬ π’ β€ π β π’ β π)) |
25 | 18, 24 | bitrd 279 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (Β¬ π’ β€ (π β¨ π) β π’ β π)) |
26 | 10, 25 | mpbird 257 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β Β¬ π’ β€ (π β¨ π)) |
27 | | simpl32 1256 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β Β¬ π£ β€ (π β¨ π’)) |
28 | 16 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β ((π β¨ π) β¨ π’) = (π β¨ π’)) |
29 | 28 | breq2d 5122 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β (π£ β€ ((π β¨ π) β¨ π’) β π£ β€ (π β¨ π’))) |
30 | 27, 29 | mtbird 325 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β Β¬ π£ β€ ((π β¨ π) β¨ π’)) |
31 | | breq1 5113 |
. . . . . . . . . . . 12
β’ (π = π’ β (π β€ (π β¨ π) β π’ β€ (π β¨ π))) |
32 | 31 | notbid 318 |
. . . . . . . . . . 11
β’ (π = π’ β (Β¬ π β€ (π β¨ π) β Β¬ π’ β€ (π β¨ π))) |
33 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = π’ β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π’)) |
34 | 33 | breq2d 5122 |
. . . . . . . . . . . 12
β’ (π = π’ β (π β€ ((π β¨ π) β¨ π) β π β€ ((π β¨ π) β¨ π’))) |
35 | 34 | notbid 318 |
. . . . . . . . . . 11
β’ (π = π’ β (Β¬ π β€ ((π β¨ π) β¨ π) β Β¬ π β€ ((π β¨ π) β¨ π’))) |
36 | 32, 35 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = π’ β ((Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π’)))) |
37 | | breq1 5113 |
. . . . . . . . . . . 12
β’ (π = π£ β (π β€ ((π β¨ π) β¨ π’) β π£ β€ ((π β¨ π) β¨ π’))) |
38 | 37 | notbid 318 |
. . . . . . . . . . 11
β’ (π = π£ β (Β¬ π β€ ((π β¨ π) β¨ π’) β Β¬ π£ β€ ((π β¨ π) β¨ π’))) |
39 | 38 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π£ β ((Β¬ π’ β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π’)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’)))) |
40 | 36, 39 | rspc2ev 3595 |
. . . . . . . . 9
β’ ((π’ β π΄ β§ π£ β π΄ β§ (Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
41 | 6, 7, 26, 30, 40 | syl112anc 1375 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π = π) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
42 | | simp22 1208 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π£ β π΄) |
43 | | simp23 1209 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β π€ β π΄) |
44 | 42, 43 | jca 513 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π£ β π΄ β§ π€ β π΄)) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β (π£ β π΄ β§ π€ β π΄)) |
46 | | simpll1 1213 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
47 | | simp32 1211 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β Β¬ π£ β€ (π β¨ π’)) |
48 | | simp33 1212 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β Β¬ π€ β€ ((π β¨ π’) β¨ π£)) |
49 | 21, 47, 48 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π’ β π΄ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
50 | 49 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β (π’ β π΄ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
51 | | simplr 768 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β π β π) |
52 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β π β€ (π β¨ π’)) |
53 | 1, 2, 3 | 3dimlem2 37951 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β§ (π β π β§ π β€ (π β¨ π’))) β (π β π β§ Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) |
54 | 46, 50, 51, 52, 53 | syl112anc 1375 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β (π β π β§ Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) |
55 | | 3simpc 1151 |
. . . . . . . . . . 11
β’ ((π β π β§ Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£)) β (Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β (Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) |
57 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π = π£ β (π β€ (π β¨ π) β π£ β€ (π β¨ π))) |
58 | 57 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π£ β (Β¬ π β€ (π β¨ π) β Β¬ π£ β€ (π β¨ π))) |
59 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = π£ β ((π β¨ π) β¨ π) = ((π β¨ π) β¨ π£)) |
60 | 59 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = π£ β (π β€ ((π β¨ π) β¨ π) β π β€ ((π β¨ π) β¨ π£))) |
61 | 60 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π£ β (Β¬ π β€ ((π β¨ π) β¨ π) β Β¬ π β€ ((π β¨ π) β¨ π£))) |
62 | 58, 61 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = π£ β ((Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (Β¬ π£ β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π£)))) |
63 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π = π€ β (π β€ ((π β¨ π) β¨ π£) β π€ β€ ((π β¨ π) β¨ π£))) |
64 | 63 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π€ β (Β¬ π β€ ((π β¨ π) β¨ π£) β Β¬ π€ β€ ((π β¨ π) β¨ π£))) |
65 | 64 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = π€ β ((Β¬ π£ β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π£)) β (Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£)))) |
66 | 62, 65 | rspc2ev 3595 |
. . . . . . . . . . 11
β’ ((π£ β π΄ β§ π€ β π΄ β§ (Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
67 | 66 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π£ β π΄ β§ π€ β π΄) β§ (Β¬ π£ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π£))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
68 | 45, 56, 67 | syl2anc 585 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ π β€ (π β¨ π’)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
69 | 21, 43 | jca 513 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π’ β π΄ β§ π€ β π΄)) |
70 | 69 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β (π’ β π΄ β§ π€ β π΄)) |
71 | | simp1 1137 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
72 | 21, 42 | jca 513 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π’ β π΄ β§ π£ β π΄)) |
73 | 8, 48 | jca 513 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π β π’ β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
74 | 71, 72, 73 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β ((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)))) |
75 | 74 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β ((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)))) |
76 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β π β π) |
77 | | simplr 768 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β Β¬ π β€ (π β¨ π’)) |
78 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β π β€ ((π β¨ π’) β¨ π£)) |
79 | 1, 2, 3 | 3dimlem3 37953 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ (π β π β§ Β¬ π β€ (π β¨ π’) β§ π β€ ((π β¨ π’) β¨ π£))) β (π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) |
80 | 75, 76, 77, 78, 79 | syl13anc 1373 |
. . . . . . . . . . . 12
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β (π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) |
81 | | 3simpc 1151 |
. . . . . . . . . . . 12
β’ ((π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) |
83 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π = π€ β (π β€ ((π β¨ π) β¨ π’) β π€ β€ ((π β¨ π) β¨ π’))) |
84 | 83 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π = π€ β (Β¬ π β€ ((π β¨ π) β¨ π’) β Β¬ π€ β€ ((π β¨ π) β¨ π’))) |
85 | 84 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π€ β ((Β¬ π’ β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π’)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’)))) |
86 | 36, 85 | rspc2ev 3595 |
. . . . . . . . . . . 12
β’ ((π’ β π΄ β§ π€ β π΄ β§ (Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
87 | 86 | 3expa 1119 |
. . . . . . . . . . 11
β’ (((π’ β π΄ β§ π€ β π΄) β§ (Β¬ π’ β€ (π β¨ π) β§ Β¬ π€ β€ ((π β¨ π) β¨ π’))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
88 | 70, 82, 87 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ π β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
89 | 72 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β (π’ β π΄ β§ π£ β π΄)) |
90 | 8, 47 | jca 513 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β (π β π’ β§ Β¬ π£ β€ (π β¨ π’))) |
91 | 71, 72, 90 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β ((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’)))) |
92 | 91 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β ((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’)))) |
93 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β π β π) |
94 | | simplr 768 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β Β¬ π β€ (π β¨ π’)) |
95 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β Β¬ π β€ ((π β¨ π’) β¨ π£)) |
96 | 1, 2, 3 | 3dimlem4 37956 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’))) β§ (π β π β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β (π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) |
97 | 92, 93, 94, 95, 96 | syl121anc 1376 |
. . . . . . . . . . . 12
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β (π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) |
98 | | 3simpc 1151 |
. . . . . . . . . . . 12
β’ ((π β π β§ Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . 11
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β (Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) |
100 | 40 | 3expa 1119 |
. . . . . . . . . . 11
β’ (((π’ β π΄ β§ π£ β π΄) β§ (Β¬ π’ β€ (π β¨ π) β§ Β¬ π£ β€ ((π β¨ π) β¨ π’))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
101 | 89, 99, 100 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β§ Β¬ π β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
102 | 88, 101 | pm2.61dan 812 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β§ Β¬ π β€ (π β¨ π’)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
103 | 68, 102 | pm2.61dan 812 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β§ π β π) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
104 | 41, 103 | pm2.61dane 3033 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
105 | 104 | 3exp 1120 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β ((π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))) |
106 | 105 | 3expd 1354 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π’ β π΄ β (π£ β π΄ β (π€ β π΄ β ((π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))))) |
107 | 106 | imp32 420 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄)) β (π€ β π΄ β ((π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))) |
108 | 107 | rexlimdv 3151 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π’ β π΄ β§ π£ β π΄)) β (βπ€ β π΄ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)))) |
109 | 108 | rexlimdvva 3206 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)))) |
110 | 5, 109 | mpd 15 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |