Step | Hyp | Ref
| Expression |
1 | | cnextval 23428 |
. . 3
β’ ((π½ β Top β§ πΎ β Top) β (π½CnExtπΎ) = (π β (βͺ πΎ βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) |
2 | 1 | adantr 482 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β (π½CnExtπΎ) = (π β (βͺ πΎ βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) |
3 | | simpr 486 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β π = πΉ) |
4 | 3 | dmeqd 5866 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β dom π = dom πΉ) |
5 | | simplrl 776 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β πΉ:π΄βΆπ΅) |
6 | 5 | fdmd 6684 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β dom πΉ = π΄) |
7 | 4, 6 | eqtrd 2777 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β dom π = π΄) |
8 | 7 | fveq2d 6851 |
. . 3
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β ((clsβπ½)βdom π) = ((clsβπ½)βπ΄)) |
9 | 7 | oveq2d 7378 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β (((neiβπ½)β{π₯}) βΎt dom π) = (((neiβπ½)β{π₯}) βΎt π΄)) |
10 | 9 | oveq2d 7378 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π)) = (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))) |
11 | 10, 3 | fveq12d 6854 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ) = ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
12 | 11 | xpeq2d 5668 |
. . 3
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) = ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
13 | 8, 12 | iuneq12d 4987 |
. 2
β’ ((((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β§ π = πΉ) β βͺ
π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
14 | | uniexg 7682 |
. . . 4
β’ (πΎ β Top β βͺ πΎ
β V) |
15 | 14 | ad2antlr 726 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β βͺ πΎ β V) |
16 | | uniexg 7682 |
. . . 4
β’ (π½ β Top β βͺ π½
β V) |
17 | 16 | ad2antrr 725 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β βͺ π½ β V) |
18 | | eqid 2737 |
. . . . . 6
β’ π΄ = π΄ |
19 | | cnextfval.2 |
. . . . . 6
β’ π΅ = βͺ
πΎ |
20 | 18, 19 | feq23i 6667 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βΆβͺ πΎ) |
21 | 20 | biimpi 215 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βΆβͺ πΎ) |
22 | 21 | ad2antrl 727 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β πΉ:π΄βΆβͺ πΎ) |
23 | | cnextfval.1 |
. . . . . 6
β’ π = βͺ
π½ |
24 | 23 | sseq2i 3978 |
. . . . 5
β’ (π΄ β π β π΄ β βͺ π½) |
25 | 24 | biimpi 215 |
. . . 4
β’ (π΄ β π β π΄ β βͺ π½) |
26 | 25 | ad2antll 728 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β π΄ β βͺ π½) |
27 | | elpm2r 8790 |
. . 3
β’ (((βͺ πΎ
β V β§ βͺ π½ β V) β§ (πΉ:π΄βΆβͺ πΎ β§ π΄ β βͺ π½)) β πΉ β (βͺ πΎ βpm βͺ π½)) |
28 | 15, 17, 22, 26, 27 | syl22anc 838 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β πΉ β (βͺ πΎ βpm βͺ π½)) |
29 | | fvex 6860 |
. . . 4
β’
((clsβπ½)βπ΄) β V |
30 | | vsnex 5391 |
. . . . 5
β’ {π₯} β V |
31 | | fvex 6860 |
. . . . 5
β’ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β V |
32 | 30, 31 | xpex 7692 |
. . . 4
β’ ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β V |
33 | 29, 32 | iunex 7906 |
. . 3
β’ βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β V |
34 | 33 | a1i 11 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β V) |
35 | 2, 13, 28, 34 | fvmptd 6960 |
1
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |