Step | Hyp | Ref
| Expression |
1 | | cvrval3.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . . . . 6
β’
(ltβπΎ) =
(ltβπΎ) |
3 | | cvrval3.c |
. . . . . 6
β’ πΆ = ( β βπΎ) |
4 | 1, 2, 3 | cvrlt 37778 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π(ltβπΎ)π) |
5 | | cvrval3.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
6 | | cvrval3.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
7 | | cvrval3.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
8 | 1, 5, 2, 6, 3, 7 | hlrelat3 37921 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π(ltβπΎ)π) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) |
9 | 4, 8 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) |
10 | | simp3l 1202 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β ππΆ(π β¨ π)) |
11 | | simp1l1 1267 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β πΎ β HL) |
12 | | simp1l2 1268 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β π β π΅) |
13 | | simp2 1138 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β π β π΄) |
14 | 1, 5, 6, 3, 7 | cvr1 37919 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) |
15 | 11, 12, 13, 14 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β (Β¬ π β€ π β ππΆ(π β¨ π))) |
16 | 10, 15 | mpbird 257 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β Β¬ π β€ π) |
17 | 11 | hllatd 37872 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β πΎ β Lat) |
18 | 1, 7 | atbase 37797 |
. . . . . . . . . . 11
β’ (π β π΄ β π β π΅) |
19 | 18 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β π β π΅) |
20 | 1, 6 | latjcl 18333 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
21 | 17, 12, 19, 20 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β (π β¨ π) β π΅) |
22 | 1, 2, 3 | cvrlt 37778 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ (π β¨ π) β π΅) β§ ππΆ(π β¨ π)) β π(ltβπΎ)(π β¨ π)) |
23 | 11, 12, 21, 10, 22 | syl31anc 1374 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β π(ltβπΎ)(π β¨ π)) |
24 | | simp3r 1203 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β (π β¨ π) β€ π) |
25 | | hlpos 37874 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β Poset) |
26 | 11, 25 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β πΎ β Poset) |
27 | | simp1l3 1269 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β π β π΅) |
28 | | simp1r 1199 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β ππΆπ) |
29 | 1, 5, 2, 3 | cvrnbtwn2 37783 |
. . . . . . . . 9
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ (π β¨ π) β π΅) β§ ππΆπ) β ((π(ltβπΎ)(π β¨ π) β§ (π β¨ π) β€ π) β (π β¨ π) = π)) |
30 | 26, 12, 27, 21, 28, 29 | syl131anc 1384 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β ((π(ltβπΎ)(π β¨ π) β§ (π β¨ π) β€ π) β (π β¨ π) = π)) |
31 | 23, 24, 30 | mpbi2and 711 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β (π β¨ π) = π) |
32 | 16, 31 | jca 513 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π΄ β§ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) β (Β¬ π β€ π β§ (π β¨ π) = π)) |
33 | 32 | 3exp 1120 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π΄ β ((ππΆ(π β¨ π) β§ (π β¨ π) β€ π) β (Β¬ π β€ π β§ (π β¨ π) = π)))) |
34 | 33 | reximdvai 3159 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) |
35 | 9, 34 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π)) |
36 | 35 | ex 414 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) |
37 | | simp3l 1202 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β Β¬ π β€ π) |
38 | | simp11 1204 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β πΎ β HL) |
39 | | simp12 1205 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β π β π΅) |
40 | | simp2 1138 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β π β π΄) |
41 | 38, 39, 40, 14 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β (Β¬ π β€ π β ππΆ(π β¨ π))) |
42 | 37, 41 | mpbid 231 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β ππΆ(π β¨ π)) |
43 | | simp3r 1203 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β (π β¨ π) = π) |
44 | 42, 43 | breqtrd 5132 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = π)) β ππΆπ) |
45 | 44 | rexlimdv3a 3153 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π) β ππΆπ)) |
46 | 36, 45 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) |