Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β πΎ β AtLat) |
2 | | atlen0.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
3 | | atlen0.z |
. . . . . 6
β’ 0 =
(0.βπΎ) |
4 | 2, 3 | atl0cl 37811 |
. . . . 5
β’ (πΎ β AtLat β 0 β π΅) |
5 | 1, 4 | syl 17 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β 0 β π΅) |
6 | | simpl2 1193 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β π΅) |
7 | 1, 5, 6 | 3jca 1129 |
. . 3
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β (πΎ β AtLat β§ 0 β π΅ β§ π β π΅)) |
8 | | simpl3 1194 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β π΄) |
9 | | atlen0.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
10 | 2, 9 | atbase 37797 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
11 | 8, 10 | syl 17 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β π΅) |
12 | | eqid 2733 |
. . . . . . 7
β’ ( β
βπΎ) = ( β
βπΎ) |
13 | 3, 12, 9 | atcvr0 37796 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β 0 ( β βπΎ)π) |
14 | 1, 8, 13 | syl2anc 585 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β 0 ( β βπΎ)π) |
15 | | eqid 2733 |
. . . . . 6
β’
(ltβπΎ) =
(ltβπΎ) |
16 | 2, 15, 12 | cvrlt 37778 |
. . . . 5
β’ (((πΎ β AtLat β§ 0 β π΅ β§ π β π΅) β§ 0 ( β βπΎ)π) β 0 (ltβπΎ)π) |
17 | 1, 5, 11, 14, 16 | syl31anc 1374 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β 0 (ltβπΎ)π) |
18 | | simpr 486 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β€ π) |
19 | | atlpos 37809 |
. . . . . 6
β’ (πΎ β AtLat β πΎ β Poset) |
20 | 1, 19 | syl 17 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β πΎ β Poset) |
21 | | atlen0.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
22 | 2, 21, 15 | pltletr 18237 |
. . . . 5
β’ ((πΎ β Poset β§ ( 0 β π΅ β§ π β π΅ β§ π β π΅)) β (( 0 (ltβπΎ)π β§ π β€ π) β 0 (ltβπΎ)π)) |
23 | 20, 5, 11, 6, 22 | syl13anc 1373 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β (( 0 (ltβπΎ)π β§ π β€ π) β 0 (ltβπΎ)π)) |
24 | 17, 18, 23 | mp2and 698 |
. . 3
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β 0 (ltβπΎ)π) |
25 | 15 | pltne 18228 |
. . 3
β’ ((πΎ β AtLat β§ 0 β π΅ β§ π β π΅) β ( 0 (ltβπΎ)π β 0 β π)) |
26 | 7, 24, 25 | sylc 65 |
. 2
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β 0 β π) |
27 | 26 | necomd 2996 |
1
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ π β€ π) β π β 0 ) |