Step | Hyp | Ref
| Expression |
1 | | dalem.ps |
. . . . 5
β’ (π β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ π β§ (π β π β§ Β¬ π β€ π β§ πΆ β€ (π β¨ π)))) |
2 | 1 | dalemddea 38193 |
. . . 4
β’ (π β π β π΄) |
3 | 1 | dalemccea 38192 |
. . . 4
β’ (π β π β π΄) |
4 | 2, 3 | jca 513 |
. . 3
β’ (π β (π β π΄ β§ π β π΄)) |
5 | 4 | 3ad2ant3 1136 |
. 2
β’ ((π β§ π = π β§ π) β (π β π΄ β§ π β π΄)) |
6 | 1 | dalem-ddly 38195 |
. . . 4
β’ (π β Β¬ π β€ π) |
7 | 6 | 3ad2ant3 1136 |
. . 3
β’ ((π β§ π = π β§ π) β Β¬ π β€ π) |
8 | | simp2 1138 |
. . . 4
β’ ((π β§ π = π β§ π) β π = π) |
9 | 8 | breq2d 5118 |
. . 3
β’ ((π β§ π = π β§ π) β (π β€ π β π β€ π)) |
10 | 7, 9 | mtbid 324 |
. 2
β’ ((π β§ π = π β§ π) β Β¬ π β€ π) |
11 | 1 | dalemccnedd 38196 |
. . . 4
β’ (π β π β π) |
12 | 11 | 3ad2ant3 1136 |
. . 3
β’ ((π β§ π = π β§ π) β π β π) |
13 | 1 | dalem-ccly 38194 |
. . . . 5
β’ (π β Β¬ π β€ π) |
14 | 13 | 3ad2ant3 1136 |
. . . 4
β’ ((π β§ π = π β§ π) β Β¬ π β€ π) |
15 | 8 | breq2d 5118 |
. . . 4
β’ ((π β§ π = π β§ π) β (π β€ π β π β€ π)) |
16 | 14, 15 | mtbid 324 |
. . 3
β’ ((π β§ π = π β§ π) β Β¬ π β€ π) |
17 | 1 | dalemclccjdd 38197 |
. . . . 5
β’ (π β πΆ β€ (π β¨ π)) |
18 | 17 | 3ad2ant3 1136 |
. . . 4
β’ ((π β§ π = π β§ π) β πΆ β€ (π β¨ π)) |
19 | | dalem.ph |
. . . . . . 7
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π))))) |
20 | 19 | dalemkehl 38132 |
. . . . . 6
β’ (π β πΎ β HL) |
21 | 20 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π = π β§ π) β πΎ β HL) |
22 | 3 | 3ad2ant3 1136 |
. . . . 5
β’ ((π β§ π = π β§ π) β π β π΄) |
23 | 2 | 3ad2ant3 1136 |
. . . . 5
β’ ((π β§ π = π β§ π) β π β π΄) |
24 | | dalem.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
25 | | dalem.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
26 | 24, 25 | hlatjcom 37876 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
27 | 21, 22, 23, 26 | syl3anc 1372 |
. . . 4
β’ ((π β§ π = π β§ π) β (π β¨ π) = (π β¨ π)) |
28 | 18, 27 | breqtrd 5132 |
. . 3
β’ ((π β§ π = π β§ π) β πΆ β€ (π β¨ π)) |
29 | 12, 16, 28 | 3jca 1129 |
. 2
β’ ((π β§ π = π β§ π) β (π β π β§ Β¬ π β€ π β§ πΆ β€ (π β¨ π))) |
30 | 5, 10, 29 | 3jca 1129 |
1
β’ ((π β§ π = π β§ π) β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ π β§ (π β π β§ Β¬ π β€ π β§ πΆ β€ (π β¨ π)))) |