Step | Hyp | Ref
| Expression |
1 | | ovexd 7393 |
. 2
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β V) |
2 | | eqid 2733 |
. . . . . . 7
β’ (πΉ βΎs π΄) = (πΉ βΎs π΄) |
3 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΉ) =
(BaseβπΉ) |
4 | 2, 3 | ressbas 17123 |
. . . . . 6
β’ (π΄ β π β (π΄ β© (BaseβπΉ)) = (Baseβ(πΉ βΎs π΄))) |
5 | | inss2 4190 |
. . . . . 6
β’ (π΄ β© (BaseβπΉ)) β (BaseβπΉ) |
6 | 4, 5 | eqsstrrdi 4000 |
. . . . 5
β’ (π΄ β π β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
7 | 6 | adantl 483 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
8 | | eqid 2733 |
. . . . . . 7
β’
(leβπΉ) =
(leβπΉ) |
9 | 3, 8 | ispos 18208 |
. . . . . 6
β’ (πΉ β Poset β (πΉ β V β§ βπ₯ β (BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
10 | 9 | simprbi 498 |
. . . . 5
β’ (πΉ β Poset β
βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§))) |
11 | 10 | adantr 482 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β βπ₯ β (BaseβπΉ)βπ¦ β (BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§))) |
12 | | ssralv 4011 |
. . . . . . . 8
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ§ β
(BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
13 | 12 | ralimdv 3163 |
. . . . . . 7
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ¦ β
(BaseβπΉ)βπ§ β (BaseβπΉ)(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)) β βπ¦ β (BaseβπΉ)βπ§ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π₯ β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β§ ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§)))) |
14 | | ssralv 4011 |
. . . . . . 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 3163 |
. . . . 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 4011 |
. . . . 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 17266 |
. . . . 5
β’ (π΄ β π β (leβπΉ) = (leβ(πΉ βΎs π΄))) |
21 | 20 | adantl 483 |
. . . 4
β’ ((πΉ β Poset β§ π΄ β π) β (leβπΉ) = (leβ(πΉ βΎs π΄))) |
22 | | breq 5108 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π₯ β π₯(leβ(πΉ βΎs π΄))π₯)) |
23 | | breq 5108 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π¦ β π₯(leβ(πΉ βΎs π΄))π¦)) |
24 | | breq 5108 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π¦(leβπΉ)π₯ β π¦(leβ(πΉ βΎs π΄))π₯)) |
25 | 23, 24 | anbi12d 632 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β (π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯))) |
26 | 25 | imbi1d 342 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π₯) β π₯ = π¦) β ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π₯) β π₯ = π¦))) |
27 | | breq 5108 |
. . . . . . . . 9
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π¦(leβπΉ)π§ β π¦(leβ(πΉ βΎs π΄))π§)) |
28 | 23, 27 | anbi12d 632 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β ((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β (π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§))) |
29 | | breq 5108 |
. . . . . . . 8
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (π₯(leβπΉ)π§ β π₯(leβ(πΉ βΎs π΄))π§)) |
30 | 28, 29 | imbi12d 345 |
. . . . . . 7
β’
((leβπΉ) =
(leβ(πΉ
βΎs π΄))
β (((π₯(leβπΉ)π¦ β§ π¦(leβπΉ)π§) β π₯(leβπΉ)π§) β ((π₯(leβ(πΉ βΎs π΄))π¦ β§ π¦(leβ(πΉ βΎs π΄))π§) β π₯(leβ(πΉ βΎs π΄))π§))) |
31 | 22, 26, 30 | 3anbi123d 1437 |
. . . . . 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 3171 |
. . . . 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 3209 |
. . . 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 2733 |
. . 3
β’
(Baseβ(πΉ
βΎs π΄)) =
(Baseβ(πΉ
βΎs π΄)) |
37 | | eqid 2733 |
. . 3
β’
(leβ(πΉ
βΎs π΄)) =
(leβ(πΉ
βΎs π΄)) |
38 | 36, 37 | ispos 18208 |
. 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 584 |
1
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) |