Step | Hyp | Ref
| Expression |
1 | | oveq1 7418 |
. . . . 5
β’ (π = π β (π β¨ π§) = (π β¨ π§)) |
2 | 1 | eqeq1d 2734 |
. . . 4
β’ (π = π β ((π β¨ π§) = (π β¨ π§) β (π β¨ π§) = (π β¨ π§))) |
3 | 2 | anbi2d 629 |
. . 3
β’ (π = π β ((Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)))) |
4 | 3 | rexbidv 3178 |
. 2
β’ (π = π β (βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)))) |
5 | | simpl1 1191 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β (πΎ β HL β§ π β π»)) |
6 | | simpl23 1253 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β (π β π΄ β§ Β¬ π β€ π)) |
7 | | simpl21 1251 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simpl32 1255 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β π β π΄) |
9 | | simpr 485 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β π β π) |
10 | | simpl22 1252 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β (π β π΄ β§ Β¬ π β€ π)) |
11 | | simp23l 1294 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
12 | 11 | adantr 481 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β π β π΄) |
13 | | simpl31 1254 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β π β π) |
14 | | simpl33 1256 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
15 | | 4that.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
16 | | 4that.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
17 | | 4that.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
18 | | 4that.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
19 | 15, 16, 17, 18 | 4atex 39250 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ¦ β π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦))) |
20 | 5, 7, 10, 12, 13, 14, 19 | syl132anc 1388 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β βπ¦ β π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦))) |
21 | | eqcom 2739 |
. . . . . 6
β’ ((π β¨ π¦) = (π β¨ π¦) β (π β¨ π¦) = (π β¨ π¦)) |
22 | 21 | anbi2i 623 |
. . . . 5
β’ ((Β¬
π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦)) β (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦))) |
23 | 22 | rexbii 3094 |
. . . 4
β’
(βπ¦ β
π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦)) β βπ¦ β π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦))) |
24 | 20, 23 | sylib 217 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β βπ¦ β π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦))) |
25 | 15, 16, 17, 18 | 4atex 39250 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ βπ¦ β π΄ (Β¬ π¦ β€ π β§ (π β¨ π¦) = (π β¨ π¦)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
26 | 5, 6, 7, 8, 9, 24,
25 | syl132anc 1388 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π β π) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
27 | | simp1 1136 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
28 | | simp21 1206 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | | simp22 1207 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
30 | | simp32 1210 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
31 | | simp31 1209 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π) |
32 | | simp33 1211 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
33 | 15, 16, 17, 18 | 4atex 39250 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
34 | 27, 28, 29, 30, 31, 32, 33 | syl132anc 1388 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
35 | 4, 26, 34 | pm2.61ne 3027 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β π΄ β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |