Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. 2
β’ (πΉ β π β πΉ β V) |
2 | | ipoval.i |
. . 3
β’ πΌ = (toIncβπΉ) |
3 | | vex 3448 |
. . . . . . . 8
β’ π β V |
4 | 3, 3 | xpex 7688 |
. . . . . . 7
β’ (π Γ π) β V |
5 | | simpl 484 |
. . . . . . . . . 10
β’ (({π₯, π¦} β π β§ π₯ β π¦) β {π₯, π¦} β π) |
6 | | vex 3448 |
. . . . . . . . . . 11
β’ π₯ β V |
7 | | vex 3448 |
. . . . . . . . . . 11
β’ π¦ β V |
8 | 6, 7 | prss 4781 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β {π₯, π¦} β π) |
9 | 5, 8 | sylibr 233 |
. . . . . . . . 9
β’ (({π₯, π¦} β π β§ π₯ β π¦) β (π₯ β π β§ π¦ β π)) |
10 | 9 | ssopab2i 5508 |
. . . . . . . 8
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} β {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)} |
11 | | df-xp 5640 |
. . . . . . . 8
β’ (π Γ π) = {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)} |
12 | 10, 11 | sseqtrri 3982 |
. . . . . . 7
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} β (π Γ π) |
13 | 4, 12 | ssexi 5280 |
. . . . . 6
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} β V |
14 | 13 | a1i 11 |
. . . . 5
β’ (π = πΉ β {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} β V) |
15 | | sseq2 3971 |
. . . . . . . 8
β’ (π = πΉ β ({π₯, π¦} β π β {π₯, π¦} β πΉ)) |
16 | 15 | anbi1d 631 |
. . . . . . 7
β’ (π = πΉ β (({π₯, π¦} β π β§ π₯ β π¦) β ({π₯, π¦} β πΉ β§ π₯ β π¦))) |
17 | 16 | opabbidv 5172 |
. . . . . 6
β’ (π = πΉ β {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} = {β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)}) |
18 | | ipoval.l |
. . . . . 6
β’ β€ =
{β¨π₯, π¦β© β£ ({π₯, π¦} β πΉ β§ π₯ β π¦)} |
19 | 17, 18 | eqtr4di 2791 |
. . . . 5
β’ (π = πΉ β {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} = β€ ) |
20 | | simpl 484 |
. . . . . . . 8
β’ ((π = πΉ β§ π = β€ ) β π = πΉ) |
21 | 20 | opeq2d 4838 |
. . . . . . 7
β’ ((π = πΉ β§ π = β€ ) β
β¨(Baseβndx), πβ© = β¨(Baseβndx), πΉβ©) |
22 | | simpr 486 |
. . . . . . . . 9
β’ ((π = πΉ β§ π = β€ ) β π = β€ ) |
23 | 22 | fveq2d 6847 |
. . . . . . . 8
β’ ((π = πΉ β§ π = β€ ) β
(ordTopβπ) =
(ordTopβ β€ )) |
24 | 23 | opeq2d 4838 |
. . . . . . 7
β’ ((π = πΉ β§ π = β€ ) β
β¨(TopSetβndx), (ordTopβπ)β© = β¨(TopSetβndx),
(ordTopβ β€
)β©) |
25 | 21, 24 | preq12d 4703 |
. . . . . 6
β’ ((π = πΉ β§ π = β€ ) β
{β¨(Baseβndx), πβ©, β¨(TopSetβndx),
(ordTopβπ)β©} =
{β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€
)β©}) |
26 | 22 | opeq2d 4838 |
. . . . . . 7
β’ ((π = πΉ β§ π = β€ ) β
β¨(leβndx), πβ© = β¨(leβndx), β€
β©) |
27 | | id 22 |
. . . . . . . . . 10
β’ (π = πΉ β π = πΉ) |
28 | | rabeq 3420 |
. . . . . . . . . . 11
β’ (π = πΉ β {π¦ β π β£ (π¦ β© π₯) = β
} = {π¦ β πΉ β£ (π¦ β© π₯) = β
}) |
29 | 28 | unieqd 4880 |
. . . . . . . . . 10
β’ (π = πΉ β βͺ {π¦ β π β£ (π¦ β© π₯) = β
} = βͺ
{π¦ β πΉ β£ (π¦ β© π₯) = β
}) |
30 | 27, 29 | mpteq12dv 5197 |
. . . . . . . . 9
β’ (π = πΉ β (π₯ β π β¦ βͺ {π¦ β π β£ (π¦ β© π₯) = β
}) = (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π = πΉ β§ π = β€ ) β (π₯ β π β¦ βͺ {π¦ β π β£ (π¦ β© π₯) = β
}) = (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})) |
32 | 31 | opeq2d 4838 |
. . . . . . 7
β’ ((π = πΉ β§ π = β€ ) β
β¨(ocβndx), (π₯
β π β¦ βͺ {π¦
β π β£ (π¦ β© π₯) = β
})β© = β¨(ocβndx),
(π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©) |
33 | 26, 32 | preq12d 4703 |
. . . . . 6
β’ ((π = πΉ β§ π = β€ ) β
{β¨(leβndx), πβ©, β¨(ocβndx), (π₯ β π β¦ βͺ {π¦ β π β£ (π¦ β© π₯) = β
})β©} = {β¨(leβndx),
β€
β©, β¨(ocβndx), (π₯ β πΉ β¦ βͺ {π¦ β πΉ β£ (π¦ β© π₯) = β
})β©}) |
34 | 25, 33 | uneq12d 4125 |
. . . . 5
β’ ((π = πΉ β§ π = β€ ) β
({β¨(Baseβndx), πβ©, β¨(TopSetβndx),
(ordTopβπ)β©}
βͺ {β¨(leβndx), πβ©, β¨(ocβndx), (π₯ β π β¦ βͺ {π¦ β π β£ (π¦ β© π₯) = β
})β©}) =
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©})) |
35 | 14, 19, 34 | csbied2 3896 |
. . . 4
β’ (π = πΉ β β¦{β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} / πβ¦({β¨(Baseβndx),
πβ©,
β¨(TopSetβndx), (ordTopβπ)β©} βͺ {β¨(leβndx), πβ©, β¨(ocβndx),
(π₯ β π β¦ βͺ {π¦
β π β£ (π¦ β© π₯) = β
})β©}) =
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©})) |
36 | | df-ipo 18422 |
. . . 4
β’ toInc =
(π β V β¦
β¦{β¨π₯,
π¦β© β£ ({π₯, π¦} β π β§ π₯ β π¦)} / πβ¦({β¨(Baseβndx),
πβ©,
β¨(TopSetβndx), (ordTopβπ)β©} βͺ {β¨(leβndx), πβ©, β¨(ocβndx),
(π₯ β π β¦ βͺ {π¦
β π β£ (π¦ β© π₯) = β
})β©})) |
37 | | prex 5390 |
. . . . 5
β’
{β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€ )β©} β
V |
38 | | prex 5390 |
. . . . 5
β’
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©} β
V |
39 | 37, 38 | unex 7681 |
. . . 4
β’
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©}) β
V |
40 | 35, 36, 39 | fvmpt 6949 |
. . 3
β’ (πΉ β V β
(toIncβπΉ) =
({β¨(Baseβndx), πΉβ©, β¨(TopSetβndx),
(ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©})) |
41 | 2, 40 | eqtrid 2785 |
. 2
β’ (πΉ β V β πΌ = ({β¨(Baseβndx),
πΉβ©,
β¨(TopSetβndx), (ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©})) |
42 | 1, 41 | syl 17 |
1
β’ (πΉ β π β πΌ = ({β¨(Baseβndx), πΉβ©,
β¨(TopSetβndx), (ordTopβ β€ )β©} βͺ
{β¨(leβndx), β€ β©,
β¨(ocβndx), (π₯
β πΉ β¦ βͺ {π¦
β πΉ β£ (π¦ β© π₯) = β
})β©})) |