Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . 7
β’ (({π₯, π¦} β πΉ β§ π₯ β π¦) β {π₯, π¦} β πΉ) |
2 | | vex 3478 |
. . . . . . . 8
β’ π₯ β V |
3 | | vex 3478 |
. . . . . . . 8
β’ π¦ β V |
4 | 2, 3 | prss 4822 |
. . . . . . 7
β’ ((π₯ β πΉ β§ π¦ β πΉ) β {π₯, π¦} β πΉ) |
5 | 1, 4 | sylibr 233 |
. . . . . 6
β’ (({π₯, π¦} β πΉ β§ π₯ β π¦) β (π₯ β πΉ β§ π¦ β πΉ)) |
6 | 5 | ssopab2i 5549 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β {β¨π₯, π¦β© β£ (π₯ β πΉ β§ π¦ β πΉ)} |
7 | | df-xp 5681 |
. . . . 5
β’ (πΉ Γ πΉ) = {β¨π₯, π¦β© β£ (π₯ β πΉ β§ π¦ β πΉ)} |
8 | 6, 7 | sseqtrri 4018 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β (πΉ Γ πΉ) |
9 | | sqxpexg 7738 |
. . . 4
β’ (πΉ β π β (πΉ Γ πΉ) β V) |
10 | | ssexg 5322 |
. . . 4
β’
(({β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β (πΉ Γ πΉ) β§ (πΉ Γ πΉ) β V) β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β V) |
11 | 8, 9, 10 | sylancr 587 |
. . 3
β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} β V) |
12 | | ipostr 18478 |
. . . 4
β’
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ{β¨π₯,
π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) Struct β¨1, ;11β© |
13 | | pleid 17308 |
. . . 4
β’ le = Slot
(leβndx) |
14 | | snsspr1 4816 |
. . . . 5
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©} β {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©} |
15 | | ssun2 4172 |
. . . . 5
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©} β
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ{β¨π₯,
π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) |
16 | 14, 15 | sstri 3990 |
. . . 4
β’
{β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©} β ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) |
17 | 12, 13, 16 | strfv 17133 |
. . 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 2732 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} |
21 | 19, 20 | ipoval 18479 |
. . 3
β’ (πΉ β π β πΌ = ({β¨(Baseβndx), πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©})) |
22 | 21 | fveq2d 6892 |
. 2
β’ (πΉ β π β (leβπΌ) = (leβ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)})β©} βͺ {β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}))) |
23 | 18, 22 | eqtr4d 2775 |
1
β’ (πΉ β π β {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} = (leβπΌ)) |