Step | Hyp | Ref
| Expression |
1 | | ovexd 7440 |
. 2
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β V) |
2 | | eqid 2732 |
. . . . . . 7
β’ (πΉ βΎs π΄) = (πΉ βΎs π΄) |
3 | | eqid 2732 |
. . . . . . 7
β’
(BaseβπΉ) =
(BaseβπΉ) |
4 | 2, 3 | ressbas 17175 |
. . . . . 6
β’ (π΄ β π β (π΄ β© (BaseβπΉ)) = (Baseβ(πΉ βΎs π΄))) |
5 | | inss2 4228 |
. . . . . 6
β’ (π΄ β© (BaseβπΉ)) β (BaseβπΉ) |
6 | 4, 5 | eqsstrrdi 4036 |
. . . . 5
β’ (π΄ β π β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
7 | 6 | adantl 482 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
8 | | eqid 2732 |
. . . . . . 7
β’
(leβπΉ) =
(leβπΉ) |
9 | 3, 8 | ispos 18263 |
. . . . . 6
β’ (πΉ β Poset β (πΉ β V β§ βπ₯ β (BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
10 | 9 | simprbi 497 |
. . . . 5
β’ (πΉ β Poset β
βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§))) |
11 | 10 | adantr 481 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β βπ₯ β (BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§))) |
12 | | ssralv 4049 |
. . . . . . . 8
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ§ β
(BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
13 | 12 | ralimdv 3169 |
. . . . . . 7
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ¦ β
(BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ¦ β (BaseβπΉ)βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
14 | | ssralv 4049 |
. . . . . . 7
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ¦ β
(BaseβπΉ)βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
15 | 13, 14 | syld 47 |
. . . . . 6
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ¦ β
(BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
16 | 15 | ralimdv 3169 |
. . . . 5
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ₯ β (BaseβπΉ)βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
17 | | ssralv 4049 |
. . . . 5
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(BaseβπΉ)βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
18 | 16, 17 | syld 47 |
. . . 4
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
19 | 7, 11, 18 | sylc 65 |
. . 3
β’ ((πΉ β Poset β§ π΄ β π) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§))) |
20 | 2, 8 | ressle 17321 |
. . . . 5
β’ (π΄ β π β (leβπΉ) = (leβ(πΉ βΎs π΄))) |
21 | 20 | adantl 482 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β (leβπΉ) = (leβ(πΉ βΎs π΄))) |
22 | | breq 5149 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π₯ β π₯(leβ(πΉ βΎs π΄))π₯)) |
23 | | breq 5149 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π¦ β π₯(leβ(πΉ βΎs π΄))π¦)) |
24 | | breq 5149 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π¦(leβπΉ)π₯ β π¦(leβ(πΉ βΎs π΄))π₯)) |
25 | 23, 24 | anbi12d 631 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β (π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯))) |
26 | 25 | imbi1d 341 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦))) |
27 | | breq 5149 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π¦(leβπΉ)π§ β π¦(leβ(πΉ βΎs π΄))π§)) |
28 | 23, 27 | anbi12d 631 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β (π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§))) |
29 | | breq 5149 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π§ β π₯(leβ(πΉ βΎs π΄))π§)) |
30 | 28, 29 | imbi12d 344 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§) β ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§))) |
31 | 22, 26, 30 | 3anbi123d 1436 |
. . . . . 6
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β ((π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β (π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§)))) |
32 | 31 | ralbidv 3177 |
. . . . 5
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (βπ§ β
(Baseβ(πΉ
βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§)))) |
33 | 32 | 2ralbidv 3218 |
. . . 4
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (βπ₯ β
(Baseβ(πΉ
βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§)))) |
34 | 21, 33 | syl 17 |
. . 3
β’ ((πΉ β Poset β§ π΄ β π) β (βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§)))) |
35 | 19, 34 | mpbid 231 |
. 2
β’ ((πΉ β Poset β§ π΄ β π) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§))) |
36 | | eqid 2732 |
. . 3
β’
(Baseβ(πΉ
βΎs π΄)) =
(Baseβ(πΉ
βΎs π΄)) |
37 | | eqid 2732 |
. . 3
β’
(leβ(πΉ
βΎs π΄)) =
(leβ(πΉ
βΎs π΄)) |
38 | 36, 37 | ispos 18263 |
. 2
β’ ((πΉ βΎs π΄) β Poset β ((πΉ βΎs π΄) β V β§ βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π₯ β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦) β§ ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§)))) |
39 | 1, 35, 38 | sylanbrc 583 |
1
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) |