Step | Hyp | Ref
| Expression |
1 | | tospos 18314 |
. . 3
β’ (πΉ β Toset β πΉ β Poset) |
2 | | resspos 31875 |
. . 3
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) |
3 | 1, 2 | sylan 581 |
. 2
β’ ((πΉ β Toset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) |
4 | | eqid 2733 |
. . . . . . 7
β’ (πΉ βΎs π΄) = (πΉ βΎs π΄) |
5 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΉ) =
(BaseβπΉ) |
6 | 4, 5 | ressbas 17123 |
. . . . . 6
β’ (π΄ β π β (π΄ β© (BaseβπΉ)) = (Baseβ(πΉ βΎs π΄))) |
7 | | inss2 4190 |
. . . . . 6
β’ (π΄ β© (BaseβπΉ)) β (BaseβπΉ) |
8 | 6, 7 | eqsstrrdi 4000 |
. . . . 5
β’ (π΄ β π β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
9 | 8 | adantl 483 |
. . . 4
β’ ((πΉ β Toset β§ π΄ β π) β (Baseβ(πΉ βΎs π΄)) β (BaseβπΉ)) |
10 | | eqid 2733 |
. . . . . . 7
β’
(leβπΉ) =
(leβπΉ) |
11 | 5, 10 | istos 18312 |
. . . . . 6
β’ (πΉ β Toset β (πΉ β Poset β§
βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯))) |
12 | 11 | simprbi 498 |
. . . . 5
β’ (πΉ β Toset β
βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯)) |
13 | 12 | adantr 482 |
. . . 4
β’ ((πΉ β Toset β§ π΄ β π) β βπ₯ β (BaseβπΉ)βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯)) |
14 | | ssralv 4011 |
. . . . 5
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯))) |
15 | | ssralv 4011 |
. . . . . 6
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ¦ β
(BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯))) |
16 | 15 | ralimdv 3163 |
. . . . 5
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(Baseβ(πΉ
βΎs π΄))βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯))) |
17 | 14, 16 | syld 47 |
. . . 4
β’
((Baseβ(πΉ
βΎs π΄))
β (BaseβπΉ)
β (βπ₯ β
(BaseβπΉ)βπ¦ β (BaseβπΉ)(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯))) |
18 | 9, 13, 17 | sylc 65 |
. . 3
β’ ((πΉ β Toset β§ π΄ β π) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯)) |
19 | 4, 10 | ressle 17266 |
. . . . . . 7
β’ (π΄ β π β (leβπΉ) = (leβ(πΉ βΎs π΄))) |
20 | 19 | breqd 5117 |
. . . . . 6
β’ (π΄ β π β (π₯(leβπΉ)π¦ β π₯(leβ(πΉ βΎs π΄))π¦)) |
21 | 19 | breqd 5117 |
. . . . . 6
β’ (π΄ β π β (π¦(leβπΉ)π₯ β π¦(leβ(πΉ βΎs π΄))π₯)) |
22 | 20, 21 | orbi12d 918 |
. . . . 5
β’ (π΄ β π β ((π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β (π₯(leβ(πΉ βΎs π΄))π¦ β¨ π¦(leβ(πΉ βΎs π΄))π₯))) |
23 | 22 | 2ralbidv 3209 |
. . . 4
β’ (π΄ β π β (βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π¦ β¨ π¦(leβ(πΉ βΎs π΄))π₯))) |
24 | 23 | adantl 483 |
. . 3
β’ ((πΉ β Toset β§ π΄ β π) β (βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβπΉ)π¦ β¨ π¦(leβπΉ)π₯) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π¦ β¨ π¦(leβ(πΉ βΎs π΄))π₯))) |
25 | 18, 24 | mpbid 231 |
. 2
β’ ((πΉ β Toset β§ π΄ β π) β βπ₯ β (Baseβ(πΉ βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π¦ β¨ π¦(leβ(πΉ βΎs π΄))π₯)) |
26 | | eqid 2733 |
. . 3
β’
(Baseβ(πΉ
βΎs π΄)) =
(Baseβ(πΉ
βΎs π΄)) |
27 | | eqid 2733 |
. . 3
β’
(leβ(πΉ
βΎs π΄)) =
(leβ(πΉ
βΎs π΄)) |
28 | 26, 27 | istos 18312 |
. 2
β’ ((πΉ βΎs π΄) β Toset β ((πΉ βΎs π΄) β Poset β§
βπ₯ β
(Baseβ(πΉ
βΎs π΄))βπ¦ β (Baseβ(πΉ βΎs π΄))(π₯(leβ(πΉ βΎs π΄))π¦ β¨ π¦(leβ(πΉ βΎs π΄))π₯))) |
29 | 3, 25, 28 | sylanbrc 584 |
1
β’ ((πΉ β Toset β§ π΄ β π) β (πΉ βΎs π΄) β Toset) |