Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | isatlat.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (glbβπ) = (glbβπΎ)) |
5 | | isatlat.g |
. . . . . . 7
β’ πΊ = (glbβπΎ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (glbβπ) = πΊ) |
7 | 6 | dmeqd 5862 |
. . . . 5
β’ (π = πΎ β dom (glbβπ) = dom πΊ) |
8 | 3, 7 | eleq12d 2828 |
. . . 4
β’ (π = πΎ β ((Baseβπ) β dom (glbβπ) β π΅ β dom πΊ)) |
9 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (0.βπ) = (0.βπΎ)) |
10 | | isatlat.z |
. . . . . . . 8
β’ 0 =
(0.βπΎ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (0.βπ) = 0 ) |
12 | 11 | neeq2d 3001 |
. . . . . 6
β’ (π = πΎ β (π₯ β (0.βπ) β π₯ β 0 )) |
13 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
14 | | isatlat.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = π΄) |
16 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
17 | | isatlat.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΎ β (leβπ) = β€ ) |
19 | 18 | breqd 5117 |
. . . . . . 7
β’ (π = πΎ β (π¦(leβπ)π₯ β π¦ β€ π₯)) |
20 | 15, 19 | rexeqbidv 3319 |
. . . . . 6
β’ (π = πΎ β (βπ¦ β (Atomsβπ)π¦(leβπ)π₯ β βπ¦ β π΄ π¦ β€ π₯)) |
21 | 12, 20 | imbi12d 345 |
. . . . 5
β’ (π = πΎ β ((π₯ β (0.βπ) β βπ¦ β (Atomsβπ)π¦(leβπ)π₯) β (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯))) |
22 | 3, 21 | raleqbidv 3318 |
. . . 4
β’ (π = πΎ β (βπ₯ β (Baseβπ)(π₯ β (0.βπ) β βπ¦ β (Atomsβπ)π¦(leβπ)π₯) β βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯))) |
23 | 8, 22 | anbi12d 632 |
. . 3
β’ (π = πΎ β (((Baseβπ) β dom (glbβπ) β§ βπ₯ β (Baseβπ)(π₯ β (0.βπ) β βπ¦ β (Atomsβπ)π¦(leβπ)π₯)) β (π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯)))) |
24 | | df-atl 37806 |
. . 3
β’ AtLat =
{π β Lat β£
((Baseβπ) β dom
(glbβπ) β§
βπ₯ β
(Baseβπ)(π₯ β (0.βπ) β βπ¦ β (Atomsβπ)π¦(leβπ)π₯))} |
25 | 23, 24 | elrab2 3649 |
. 2
β’ (πΎ β AtLat β (πΎ β Lat β§ (π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯)))) |
26 | | 3anass 1096 |
. 2
β’ ((πΎ β Lat β§ π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯)) β (πΎ β Lat β§ (π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯)))) |
27 | 25, 26 | bitr4i 278 |
1
β’ (πΎ β AtLat β (πΎ β Lat β§ π΅ β dom πΊ β§ βπ₯ β π΅ (π₯ β 0 β βπ¦ β π΄ π¦ β€ π₯))) |