Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
β’ (({π₯, π¦} β πΉ β§ π₯ β π¦) β {π₯, π¦} β πΉ) |
2 | | vex 3448 |
. . . . . . . 8
β’ π₯ β V |
3 | | vex 3448 |
. . . . . . . 8
β’ π¦ β V |
4 | 2, 3 | prss 4781 |
. . . . . . 7
β’ ((π₯ β πΉ β§ π¦ β πΉ) β {π₯, π¦} β πΉ) |
5 | 1, 4 | sylibr 233 |
. . . . . 6
β’ (({π₯, π¦} β πΉ β§ π₯ β π¦) β (π₯ β πΉ β§ π¦ β πΉ)) |
6 | 5 | ssopab2i 5508 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β {β¨π₯, π¦β© β£ (π₯ β πΉ β§ π¦ β πΉ)} |
7 | | df-xp 5640 |
. . . . 5
β’ (πΉ Γ πΉ) = {β¨π₯, π¦β© β£ (π₯ β πΉ β§ π¦ β πΉ)} |
8 | 6, 7 | sseqtrri 3982 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β (πΉ Γ πΉ) |
9 | | sqxpexg 7690 |
. . . 4
β’ (πΉ β π β (πΉ Γ πΉ) β V) |
10 | | ssexg 5281 |
. . . 4
β’
(({β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β (πΉ Γ πΉ) β§ (πΉ Γ πΉ) β V) β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β V) |
11 | 8, 9, 10 | sylancr 588 |
. . 3
β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β V) |
12 | | ipostr 18423 |
. . . 4
β’
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ{β¨π₯,
π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) Struct β¨1, ;11β© |
13 | | pleid 17253 |
. . . 4
β’ le = Slot
(leβndx) |
14 | | snsspr1 4775 |
. . . . 5
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©} β {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©} |
15 | | ssun2 4134 |
. . . . 5
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©} β
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ{β¨π₯,
π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) |
16 | 14, 15 | sstri 3954 |
. . . 4
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©} β ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) |
17 | 12, 13, 16 | strfv 17081 |
. . 3
β’
({β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β V β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}))) |
18 | 11, 17 | syl 17 |
. 2
β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}))) |
19 | | ipoval.i |
. . . 4
β’ πΌ = (toIncβπΉ) |
20 | | eqid 2733 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} |
21 | 19, 20 | ipoval 18424 |
. . 3
β’ (πΉ β π β πΌ = ({β¨(Baseβndx), πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©})) |
22 | 21 | fveq2d 6847 |
. 2
β’ (πΉ β π β (leβπΌ) = (leβ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}))) |
23 | 18, 22 | eqtr4d 2776 |
1
β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβπΌ)) |