Step | Hyp | Ref
| Expression |
1 | | setsval 17044 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β (π sSet β¨(πΈβndx), πΆβ©) = ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})) |
2 | 1 | fveq2d 6847 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (πΈβ(π sSet β¨(πΈβndx), πΆβ©)) = (πΈβ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}))) |
3 | | setsid.e |
. . 3
β’ πΈ = Slot (πΈβndx) |
4 | | resexg 5984 |
. . . . 5
β’ (π β π΄ β (π βΎ (V β {(πΈβndx)})) β V) |
5 | 4 | adantr 482 |
. . . 4
β’ ((π β π΄ β§ πΆ β π) β (π βΎ (V β {(πΈβndx)})) β V) |
6 | | snex 5389 |
. . . 4
β’
{β¨(πΈβndx), πΆβ©} β V |
7 | | unexg 7684 |
. . . 4
β’ (((π βΎ (V β {(πΈβndx)})) β V β§
{β¨(πΈβndx), πΆβ©} β V) β ((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) β
V) |
8 | 5, 6, 7 | sylancl 587 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) β V) |
9 | 3, 8 | strfvnd 17062 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (πΈβ((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})) = (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx))) |
10 | | fvex 6856 |
. . . . . 6
β’ (πΈβndx) β
V |
11 | 10 | snid 4623 |
. . . . 5
β’ (πΈβndx) β {(πΈβndx)} |
12 | | fvres 6862 |
. . . . 5
β’ ((πΈβndx) β {(πΈβndx)} β ((((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)})β(πΈβndx)) = (((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©})β(πΈβndx))) |
13 | 11, 12 | ax-mp 5 |
. . . 4
β’ ((((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)})β(πΈβndx)) = (((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©})β(πΈβndx)) |
14 | | resres 5951 |
. . . . . . . . 9
β’ ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) = (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) |
15 | | disjdifr 4433 |
. . . . . . . . . . 11
β’ ((V
β {(πΈβndx)})
β© {(πΈβndx)}) =
β
|
16 | 15 | reseq2i 5935 |
. . . . . . . . . 10
β’ (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) = (π βΎ
β
) |
17 | | res0 5942 |
. . . . . . . . . 10
β’ (π βΎ β
) =
β
|
18 | 16, 17 | eqtri 2761 |
. . . . . . . . 9
β’ (π βΎ ((V β {(πΈβndx)}) β© {(πΈβndx)})) =
β
|
19 | 14, 18 | eqtri 2761 |
. . . . . . . 8
β’ ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) =
β
|
20 | 19 | a1i 11 |
. . . . . . 7
β’ ((π β π΄ β§ πΆ β π) β ((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) = β
) |
21 | | elex 3462 |
. . . . . . . . . . 11
β’ (πΆ β π β πΆ β V) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π΄ β§ πΆ β π) β πΆ β V) |
23 | | opelxpi 5671 |
. . . . . . . . . 10
β’ (((πΈβndx) β V β§ πΆ β V) β β¨(πΈβndx), πΆβ© β (V Γ
V)) |
24 | 10, 22, 23 | sylancr 588 |
. . . . . . . . 9
β’ ((π β π΄ β§ πΆ β π) β β¨(πΈβndx), πΆβ© β (V Γ
V)) |
25 | | opex 5422 |
. . . . . . . . . 10
β’
β¨(πΈβndx),
πΆβ© β
V |
26 | 25 | relsn 5761 |
. . . . . . . . 9
β’ (Rel
{β¨(πΈβndx), πΆβ©} β β¨(πΈβndx), πΆβ© β (V Γ
V)) |
27 | 24, 26 | sylibr 233 |
. . . . . . . 8
β’ ((π β π΄ β§ πΆ β π) β Rel {β¨(πΈβndx), πΆβ©}) |
28 | | dmsnopss 6167 |
. . . . . . . 8
β’ dom
{β¨(πΈβndx), πΆβ©} β {(πΈβndx)} |
29 | | relssres 5979 |
. . . . . . . 8
β’ ((Rel
{β¨(πΈβndx), πΆβ©} β§ dom {β¨(πΈβndx), πΆβ©} β {(πΈβndx)}) β ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
30 | 27, 28, 29 | sylancl 587 |
. . . . . . 7
β’ ((π β π΄ β§ πΆ β π) β ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
31 | 20, 30 | uneq12d 4125 |
. . . . . 6
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) βͺ ({β¨(πΈβndx), πΆβ©} βΎ {(πΈβndx)})) = (β
βͺ
{β¨(πΈβndx), πΆβ©})) |
32 | | resundir 5953 |
. . . . . 6
β’ (((π βΎ (V β {(πΈβndx)})) βͺ
{β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)}) = (((π βΎ (V β {(πΈβndx)})) βΎ {(πΈβndx)}) βͺ
({β¨(πΈβndx),
πΆβ©} βΎ {(πΈβndx)})) |
33 | | un0 4351 |
. . . . . . 7
β’
({β¨(πΈβndx), πΆβ©} βͺ β
) = {β¨(πΈβndx), πΆβ©} |
34 | | uncom 4114 |
. . . . . . 7
β’
({β¨(πΈβndx), πΆβ©} βͺ β
) = (β
βͺ
{β¨(πΈβndx), πΆβ©}) |
35 | 33, 34 | eqtr3i 2763 |
. . . . . 6
β’
{β¨(πΈβndx), πΆβ©} = (β
βͺ {β¨(πΈβndx), πΆβ©}) |
36 | 31, 32, 35 | 3eqtr4g 2798 |
. . . . 5
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)}) = {β¨(πΈβndx), πΆβ©}) |
37 | 36 | fveq1d 6845 |
. . . 4
β’ ((π β π΄ β§ πΆ β π) β ((((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©}) βΎ {(πΈβndx)})β(πΈβndx)) = ({β¨(πΈβndx), πΆβ©}β(πΈβndx))) |
38 | 13, 37 | eqtr3id 2787 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx)) = ({β¨(πΈβndx), πΆβ©}β(πΈβndx))) |
39 | 10 | a1i 11 |
. . . 4
β’ ((π β π΄ β§ πΆ β π) β (πΈβndx) β V) |
40 | | fvsng 7127 |
. . . 4
β’ (((πΈβndx) β V β§ πΆ β π) β ({β¨(πΈβndx), πΆβ©}β(πΈβndx)) = πΆ) |
41 | 39, 40 | sylancom 589 |
. . 3
β’ ((π β π΄ β§ πΆ β π) β ({β¨(πΈβndx), πΆβ©}β(πΈβndx)) = πΆ) |
42 | 38, 41 | eqtrd 2773 |
. 2
β’ ((π β π΄ β§ πΆ β π) β (((π βΎ (V β {(πΈβndx)})) βͺ {β¨(πΈβndx), πΆβ©})β(πΈβndx)) = πΆ) |
43 | 2, 9, 42 | 3eqtrrd 2778 |
1
β’ ((π β π΄ β§ πΆ β π) β πΆ = (πΈβ(π sSet β¨(πΈβndx), πΆβ©))) |