Step | Hyp | Ref
| Expression |
1 | | ssrab2 4077 |
. . . . . . . 8
β’ {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (AtomsβπΎ) |
2 | | sseq1 4007 |
. . . . . . . 8
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (AtomsβπΎ) β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (AtomsβπΎ))) |
3 | 1, 2 | mpbiri 257 |
. . . . . . 7
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β π β (AtomsβπΎ)) |
4 | 3 | a1i 11 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β π β (AtomsβπΎ))) |
5 | | eqid 2732 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | eqid 2732 |
. . . . . . . . . 10
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
7 | 5, 6 | atbase 38154 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
8 | 5, 6 | atbase 38154 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
9 | 7, 8 | anim12i 613 |
. . . . . . . 8
β’ ((π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π β (BaseβπΎ) β§ π β (BaseβπΎ))) |
10 | | eqid 2732 |
. . . . . . . . . 10
β’
(joinβπΎ) =
(joinβπΎ) |
11 | 5, 10 | latjcl 18391 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
12 | 11 | 3expb 1120 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ))) β (π(joinβπΎ)π) β (BaseβπΎ)) |
13 | 9, 12 | sylan2 593 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π(joinβπΎ)π) β (BaseβπΎ)) |
14 | | eleq2 2822 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)})) |
15 | | breq1 5151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
16 | 15 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
17 | 5, 6 | atbase 38154 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
18 | 17 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
19 | 16, 18 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
20 | 14, 19 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
21 | | eleq2 2822 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)})) |
22 | | breq1 5151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
23 | 22 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
24 | 5, 6 | atbase 38154 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
25 | 24 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
26 | 23, 25 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
27 | 21, 26 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
28 | 20, 27 | anim12d 609 |
. . . . . . . . . . . . . . . . 17
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β ((π β π β§ π β π) β ((π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)) β§ (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))))) |
29 | | an4 654 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)) β§ (π β (BaseβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
30 | 28, 29 | imbitrdi 250 |
. . . . . . . . . . . . . . . 16
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β ((π β π β§ π β π) β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π))))) |
31 | 30 | imp 407 |
. . . . . . . . . . . . . . 15
β’ ((π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β§ (π β π β§ π β π)) β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
32 | 31 | anim2i 617 |
. . . . . . . . . . . . . 14
β’ (((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β§ (π β π β§ π β π))) β ((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π))))) |
33 | 32 | anassrs 468 |
. . . . . . . . . . . . 13
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β ((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π))))) |
34 | 5, 6 | atbase 38154 |
. . . . . . . . . . . . 13
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
35 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(leβπΎ) =
(leβπΎ) |
36 | 5, 35, 10 | latjle12 18402 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π(joinβπΎ)π) β (BaseβπΎ))) β ((π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π))) |
37 | 36 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π(joinβπΎ)π) β (BaseβπΎ))) β ((π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π))) |
38 | 37 | 3exp2 1354 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β Lat β (π β (BaseβπΎ) β (π β (BaseβπΎ) β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)))))) |
39 | 38 | impd 411 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β Lat β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π))))) |
40 | 39 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β Lat β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π))))) |
41 | 40 | imp43 428 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) |
43 | 5, 10 | latjcl 18391 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
44 | 43 | 3expib 1122 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β Lat β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π) β (BaseβπΎ))) |
45 | 5, 35 | lattr 18396 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π(joinβπΎ)π) β (BaseβπΎ) β§ (π(joinβπΎ)π) β (BaseβπΎ))) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π))) |
46 | 45 | 3exp2 1354 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β Lat β (π β (BaseβπΎ) β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π)))))) |
47 | 46 | com24 95 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β Lat β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π(joinβπΎ)π) β (BaseβπΎ) β (π β (BaseβπΎ) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π)))))) |
48 | 44, 47 | syl5d 73 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β Lat β ((π(joinβπΎ)π) β (BaseβπΎ) β ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β (BaseβπΎ) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π)))))) |
49 | 48 | imp41 426 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ))) β§ π β (BaseβπΎ)) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π))) |
50 | 49 | adantlrr 719 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) β§ π β (BaseβπΎ)) β ((π(leβπΎ)(π(joinβπΎ)π) β§ (π(joinβπΎ)π)(leβπΎ)(π(joinβπΎ)π)) β π(leβπΎ)(π(joinβπΎ)π))) |
51 | 42, 50 | mpan2d 692 |
. . . . . . . . . . . . 13
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ ((π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π(leβπΎ)(π(joinβπΎ)π) β§ π(leβπΎ)(π(joinβπΎ)π)))) β§ π β (BaseβπΎ)) β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
52 | 33, 34, 51 | syl2an 596 |
. . . . . . . . . . . 12
β’
(((((πΎ β Lat
β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β§ π β (AtomsβπΎ)) β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
53 | | simpr 485 |
. . . . . . . . . . . 12
β’
(((((πΎ β Lat
β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β§ π β (AtomsβπΎ)) β π β (AtomsβπΎ)) |
54 | 52, 53 | jctild 526 |
. . . . . . . . . . 11
β’
(((((πΎ β Lat
β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β§ π β (AtomsβπΎ)) β (π(leβπΎ)(π(joinβπΎ)π) β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
55 | | eleq2 2822 |
. . . . . . . . . . . . 13
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)})) |
56 | | breq1 5151 |
. . . . . . . . . . . . . 14
β’ (π = π β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
57 | 56 | elrab 3683 |
. . . . . . . . . . . . 13
β’ (π β {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π))) |
58 | 55, 57 | bitrdi 286 |
. . . . . . . . . . . 12
β’ (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β π β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
59 | 58 | ad3antlr 729 |
. . . . . . . . . . 11
β’
(((((πΎ β Lat
β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β§ π β (AtomsβπΎ)) β (π β π β (π β (AtomsβπΎ) β§ π(leβπΎ)(π(joinβπΎ)π)))) |
60 | 54, 59 | sylibrd 258 |
. . . . . . . . . 10
β’
(((((πΎ β Lat
β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β§ π β (AtomsβπΎ)) β (π(leβπΎ)(π(joinβπΎ)π) β π β π)) |
61 | 60 | ralrimiva 3146 |
. . . . . . . . 9
β’ ((((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β§ (π β π β§ π β π)) β βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)) |
62 | 61 | ralrimivva 3200 |
. . . . . . . 8
β’ (((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)) |
63 | 62 | ex 413 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π(joinβπΎ)π) β (BaseβπΎ)) β (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π))) |
64 | 13, 63 | syldan 591 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π))) |
65 | 4, 64 | jcad 513 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)} β (π β (AtomsβπΎ) β§ βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)))) |
66 | 65 | adantld 491 |
. . . 4
β’ ((πΎ β Lat β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((π β π β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β (π β (AtomsβπΎ) β§ βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)))) |
67 | 66 | rexlimdvva 3211 |
. . 3
β’ (πΎ β Lat β (βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}) β (π β (AtomsβπΎ) β§ βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)))) |
68 | | linepsub.n |
. . . 4
β’ π = (LinesβπΎ) |
69 | 35, 10, 6, 68 | isline 38605 |
. . 3
β’ (πΎ β Lat β (π β π β βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = {π β (AtomsβπΎ) β£ π(leβπΎ)(π(joinβπΎ)π)}))) |
70 | | linepsub.s |
. . . 4
β’ π = (PSubSpβπΎ) |
71 | 35, 10, 6, 70 | ispsubsp 38611 |
. . 3
β’ (πΎ β Lat β (π β π β (π β (AtomsβπΎ) β§ βπ β π βπ β π βπ β (AtomsβπΎ)(π(leβπΎ)(π(joinβπΎ)π) β π β π)))) |
72 | 67, 69, 71 | 3imtr4d 293 |
. 2
β’ (πΎ β Lat β (π β π β π β π)) |
73 | 72 | imp 407 |
1
β’ ((πΎ β Lat β§ π β π) β π β π) |