Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | ispos.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | 3 | eqeq2d 2744 |
. . . . 5
β’ (π = πΎ β (π = (Baseβπ) β π = π΅)) |
5 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
6 | | ispos.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (leβπ) = β€ ) |
8 | 7 | eqeq2d 2744 |
. . . . 5
β’ (π = πΎ β (π = (leβπ) β π = β€ )) |
9 | 4, 8 | 3anbi12d 1438 |
. . . 4
β’ (π = πΎ β ((π = (Baseβπ) β§ π = (leβπ) β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))) β (π = π΅ β§ π = β€ β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))))) |
10 | 9 | 2exbidv 1928 |
. . 3
β’ (π = πΎ β (βπβπ(π = (Baseβπ) β§ π = (leβπ) β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))) β βπβπ(π = π΅ β§ π = β€ β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))))) |
11 | | df-poset 18210 |
. . 3
β’ Poset =
{π β£ βπβπ(π = (Baseβπ) β§ π = (leβπ) β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))} |
12 | 10, 11 | elab4g 3639 |
. 2
β’ (πΎ β Poset β (πΎ β V β§ βπβπ(π = π΅ β§ π = β€ β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))))) |
13 | 2 | fvexi 6860 |
. . . 4
β’ π΅ β V |
14 | 6 | fvexi 6860 |
. . . 4
β’ β€ β
V |
15 | | raleq 3308 |
. . . . . 6
β’ (π = π΅ β (βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β βπ§ β π΅ (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))) |
16 | 15 | raleqbi1dv 3306 |
. . . . 5
β’ (π = π΅ β (βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β βπ¦ β π΅ βπ§ β π΅ (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))) |
17 | 16 | raleqbi1dv 3306 |
. . . 4
β’ (π = π΅ β (βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))) |
18 | | breq 5111 |
. . . . . . 7
β’ (π = β€ β (π₯ππ₯ β π₯ β€ π₯)) |
19 | | breq 5111 |
. . . . . . . . 9
β’ (π = β€ β (π₯ππ¦ β π₯ β€ π¦)) |
20 | | breq 5111 |
. . . . . . . . 9
β’ (π = β€ β (π¦ππ₯ β π¦ β€ π₯)) |
21 | 19, 20 | anbi12d 632 |
. . . . . . . 8
β’ (π = β€ β ((π₯ππ¦ β§ π¦ππ₯) β (π₯ β€ π¦ β§ π¦ β€ π₯))) |
22 | 21 | imbi1d 342 |
. . . . . . 7
β’ (π = β€ β (((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦))) |
23 | | breq 5111 |
. . . . . . . . 9
β’ (π = β€ β (π¦ππ§ β π¦ β€ π§)) |
24 | 19, 23 | anbi12d 632 |
. . . . . . . 8
β’ (π = β€ β ((π₯ππ¦ β§ π¦ππ§) β (π₯ β€ π¦ β§ π¦ β€ π§))) |
25 | | breq 5111 |
. . . . . . . 8
β’ (π = β€ β (π₯ππ§ β π₯ β€ π§)) |
26 | 24, 25 | imbi12d 345 |
. . . . . . 7
β’ (π = β€ β (((π₯ππ¦ β§ π¦ππ§) β π₯ππ§) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§))) |
27 | 18, 22, 26 | 3anbi123d 1437 |
. . . . . 6
β’ (π = β€ β ((π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |
28 | 27 | ralbidv 3171 |
. . . . 5
β’ (π = β€ β (βπ§ β π΅ (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |
29 | 28 | 2ralbidv 3209 |
. . . 4
β’ (π = β€ β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |
30 | 13, 14, 17, 29 | ceqsex2v 3501 |
. . 3
β’
(βπβπ(π = π΅ β§ π = β€ β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§))) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§))) |
31 | 30 | anbi2i 624 |
. 2
β’ ((πΎ β V β§ βπβπ(π = π΅ β§ π = β€ β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ₯ β§ ((π₯ππ¦ β§ π¦ππ₯) β π₯ = π¦) β§ ((π₯ππ¦ β§ π¦ππ§) β π₯ππ§)))) β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |
32 | 12, 31 | bitri 275 |
1
β’ (πΎ β Poset β (πΎ β V β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π₯) β π₯ = π¦) β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |