Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | isopos.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (lubβπ) = (lubβπΎ)) |
5 | | isopos.e |
. . . . . . . 8
β’ π = (lubβπΎ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (lubβπ) = π) |
7 | 6 | dmeqd 5862 |
. . . . . 6
β’ (π = πΎ β dom (lubβπ) = dom π) |
8 | 3, 7 | eleq12d 2832 |
. . . . 5
β’ (π = πΎ β ((Baseβπ) β dom (lubβπ) β π΅ β dom π)) |
9 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (glbβπ) = (glbβπΎ)) |
10 | | isopos.g |
. . . . . . . 8
β’ πΊ = (glbβπΎ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (glbβπ) = πΊ) |
12 | 11 | dmeqd 5862 |
. . . . . 6
β’ (π = πΎ β dom (glbβπ) = dom πΊ) |
13 | 3, 12 | eleq12d 2832 |
. . . . 5
β’ (π = πΎ β ((Baseβπ) β dom (glbβπ) β π΅ β dom πΊ)) |
14 | 8, 13 | anbi12d 632 |
. . . 4
β’ (π = πΎ β (((Baseβπ) β dom (lubβπ) β§ (Baseβπ) β dom (glbβπ)) β (π΅ β dom π β§ π΅ β dom πΊ))) |
15 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (ocβπ) = (ocβπΎ)) |
16 | | isopos.o |
. . . . . . . 8
β’ β₯ =
(ocβπΎ) |
17 | 15, 16 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (ocβπ) = β₯ ) |
18 | 17 | eqeq2d 2748 |
. . . . . 6
β’ (π = πΎ β (π = (ocβπ) β π = β₯ )) |
19 | 3 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = πΎ β ((πβπ₯) β (Baseβπ) β (πβπ₯) β π΅)) |
20 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
21 | | isopos.l |
. . . . . . . . . . . . 13
β’ β€ =
(leβπΎ) |
22 | 20, 21 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ (π = πΎ β (leβπ) = β€ ) |
23 | 22 | breqd 5117 |
. . . . . . . . . . 11
β’ (π = πΎ β (π₯(leβπ)π¦ β π₯ β€ π¦)) |
24 | 22 | breqd 5117 |
. . . . . . . . . . 11
β’ (π = πΎ β ((πβπ¦)(leβπ)(πβπ₯) β (πβπ¦) β€ (πβπ₯))) |
25 | 23, 24 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = πΎ β ((π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯)) β (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯)))) |
26 | 19, 25 | 3anbi13d 1439 |
. . . . . . . . 9
β’ (π = πΎ β (((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β ((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))))) |
27 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
28 | | isopos.j |
. . . . . . . . . . . 12
β’ β¨ =
(joinβπΎ) |
29 | 27, 28 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = πΎ β (joinβπ) = β¨ ) |
30 | 29 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΎ β (π₯(joinβπ)(πβπ₯)) = (π₯ β¨ (πβπ₯))) |
31 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (1.βπ) = (1.βπΎ)) |
32 | | isopos.u |
. . . . . . . . . . 11
β’ 1 =
(1.βπΎ) |
33 | 31, 32 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (1.βπ) = 1 ) |
34 | 30, 33 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = πΎ β ((π₯(joinβπ)(πβπ₯)) = (1.βπ) β (π₯ β¨ (πβπ₯)) = 1 )) |
35 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
36 | | isopos.m |
. . . . . . . . . . . 12
β’ β§ =
(meetβπΎ) |
37 | 35, 36 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = πΎ β (meetβπ) = β§ ) |
38 | 37 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΎ β (π₯(meetβπ)(πβπ₯)) = (π₯ β§ (πβπ₯))) |
39 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (0.βπ) = (0.βπΎ)) |
40 | | isopos.f |
. . . . . . . . . . 11
β’ 0 =
(0.βπΎ) |
41 | 39, 40 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (0.βπ) = 0 ) |
42 | 38, 41 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = πΎ β ((π₯(meetβπ)(πβπ₯)) = (0.βπ) β (π₯ β§ (πβπ₯)) = 0 )) |
43 | 26, 34, 42 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π = πΎ β ((((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ)) β (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))) |
44 | 3, 43 | raleqbidv 3320 |
. . . . . . 7
β’ (π = πΎ β (βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ)) β βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))) |
45 | 3, 44 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ)) β βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))) |
46 | 18, 45 | anbi12d 632 |
. . . . 5
β’ (π = πΎ β ((π = (ocβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ))) β (π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 )))) |
47 | 46 | exbidv 1925 |
. . . 4
β’ (π = πΎ β (βπ(π = (ocβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ))) β βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 )))) |
48 | 14, 47 | anbi12d 632 |
. . 3
β’ (π = πΎ β ((((Baseβπ) β dom (lubβπ) β§ (Baseβπ) β dom (glbβπ)) β§ βπ(π = (ocβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ)))) β ((π΅ β dom π β§ π΅ β dom πΊ) β§ βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))))) |
49 | | df-oposet 37641 |
. . 3
β’ OP =
{π β Poset β£
(((Baseβπ) β dom
(lubβπ) β§
(Baseβπ) β dom
(glbβπ)) β§
βπ(π = (ocβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((πβπ₯) β (Baseβπ) β§ (πβ(πβπ₯)) = π₯ β§ (π₯(leβπ)π¦ β (πβπ¦)(leβπ)(πβπ₯))) β§ (π₯(joinβπ)(πβπ₯)) = (1.βπ) β§ (π₯(meetβπ)(πβπ₯)) = (0.βπ))))} |
50 | 48, 49 | elrab2 3649 |
. 2
β’ (πΎ β OP β (πΎ β Poset β§ ((π΅ β dom π β§ π΅ β dom πΊ) β§ βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))))) |
51 | | anass 470 |
. 2
β’ (((πΎ β Poset β§ (π΅ β dom π β§ π΅ β dom πΊ)) β§ βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))) β (πΎ β Poset β§ ((π΅ β dom π β§ π΅ β dom πΊ) β§ βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))))) |
52 | | 3anass 1096 |
. . . 4
β’ ((πΎ β Poset β§ π΅ β dom π β§ π΅ β dom πΊ) β (πΎ β Poset β§ (π΅ β dom π β§ π΅ β dom πΊ))) |
53 | 52 | bicomi 223 |
. . 3
β’ ((πΎ β Poset β§ (π΅ β dom π β§ π΅ β dom πΊ)) β (πΎ β Poset β§ π΅ β dom π β§ π΅ β dom πΊ)) |
54 | 16 | fvexi 6857 |
. . . 4
β’ β₯ β
V |
55 | | fveq1 6842 |
. . . . . . . 8
β’ (π = β₯ β (πβπ₯) = ( β₯ βπ₯)) |
56 | 55 | eleq1d 2823 |
. . . . . . 7
β’ (π = β₯ β ((πβπ₯) β π΅ β ( β₯ βπ₯) β π΅)) |
57 | | id 22 |
. . . . . . . . 9
β’ (π = β₯ β π = β₯ ) |
58 | 57, 55 | fveq12d 6850 |
. . . . . . . 8
β’ (π = β₯ β (πβ(πβπ₯)) = ( β₯ β( β₯
βπ₯))) |
59 | 58 | eqeq1d 2739 |
. . . . . . 7
β’ (π = β₯ β ((πβ(πβπ₯)) = π₯ β ( β₯ β( β₯
βπ₯)) = π₯)) |
60 | | fveq1 6842 |
. . . . . . . . 9
β’ (π = β₯ β (πβπ¦) = ( β₯ βπ¦)) |
61 | 60, 55 | breq12d 5119 |
. . . . . . . 8
β’ (π = β₯ β ((πβπ¦) β€ (πβπ₯) β ( β₯ βπ¦) β€ ( β₯ βπ₯))) |
62 | 61 | imbi2d 341 |
. . . . . . 7
β’ (π = β₯ β ((π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯)) β (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯)))) |
63 | 56, 59, 62 | 3anbi123d 1437 |
. . . . . 6
β’ (π = β₯ β (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β (( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))))) |
64 | 55 | oveq2d 7374 |
. . . . . . 7
β’ (π = β₯ β (π₯ β¨ (πβπ₯)) = (π₯ β¨ ( β₯ βπ₯))) |
65 | 64 | eqeq1d 2739 |
. . . . . 6
β’ (π = β₯ β ((π₯ β¨ (πβπ₯)) = 1 β (π₯ β¨ ( β₯ βπ₯)) = 1 )) |
66 | 55 | oveq2d 7374 |
. . . . . . 7
β’ (π = β₯ β (π₯ β§ (πβπ₯)) = (π₯ β§ ( β₯ βπ₯))) |
67 | 66 | eqeq1d 2739 |
. . . . . 6
β’ (π = β₯ β ((π₯ β§ (πβπ₯)) = 0 β (π₯ β§ ( β₯ βπ₯)) = 0 )) |
68 | 63, 65, 67 | 3anbi123d 1437 |
. . . . 5
β’ (π = β₯ β ((((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ) β ((( β₯
βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ))) |
69 | 68 | 2ralbidv 3213 |
. . . 4
β’ (π = β₯ β
(βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ) β βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ))) |
70 | 54, 69 | ceqsexv 3495 |
. . 3
β’
(βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 )) β βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 )) |
71 | 53, 70 | anbi12i 628 |
. 2
β’ (((πΎ β Poset β§ (π΅ β dom π β§ π΅ β dom πΊ)) β§ βπ(π = β₯ β§ βπ₯ β π΅ βπ¦ β π΅ (((πβπ₯) β π΅ β§ (πβ(πβπ₯)) = π₯ β§ (π₯ β€ π¦ β (πβπ¦) β€ (πβπ₯))) β§ (π₯ β¨ (πβπ₯)) = 1 β§ (π₯ β§ (πβπ₯)) = 0 ))) β ((πΎ β Poset β§ π΅ β dom π β§ π΅ β dom πΊ) β§ βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ))) |
72 | 50, 51, 71 | 3bitr2i 299 |
1
β’ (πΎ β OP β ((πΎ β Poset β§ π΅ β dom π β§ π΅ β dom πΊ) β§ βπ₯ β π΅ βπ¦ β π΅ ((( β₯ βπ₯) β π΅ β§ ( β₯ β( β₯
βπ₯)) = π₯ β§ (π₯ β€ π¦ β ( β₯ βπ¦) β€ ( β₯ βπ₯))) β§ (π₯ β¨ ( β₯ βπ₯)) = 1 β§ (π₯ β§ ( β₯ βπ₯)) = 0 ))) |