Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . . . . 9
β’ (π₯ β π΄ β¦ πΎ) = (π₯ β π΄ β¦ πΎ) |
2 | 1 | fvmpt2 7006 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ πΎ β Top) β ((π₯ β π΄ β¦ πΎ)βπ₯) = πΎ) |
3 | 2 | eqcomd 2738 |
. . . . . . 7
β’ ((π₯ β π΄ β§ πΎ β Top) β πΎ = ((π₯ β π΄ β¦ πΎ)βπ₯)) |
4 | 3 | unieqd 4921 |
. . . . . 6
β’ ((π₯ β π΄ β§ πΎ β Top) β βͺ πΎ =
βͺ ((π₯ β π΄ β¦ πΎ)βπ₯)) |
5 | 4 | ralimiaa 3082 |
. . . . 5
β’
(βπ₯ β
π΄ πΎ β Top β βπ₯ β π΄ βͺ πΎ = βͺ
((π₯ β π΄ β¦ πΎ)βπ₯)) |
6 | 5 | adantl 482 |
. . . 4
β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β βπ₯ β π΄ βͺ πΎ = βͺ
((π₯ β π΄ β¦ πΎ)βπ₯)) |
7 | | ixpeq2 8901 |
. . . 4
β’
(βπ₯ β
π΄ βͺ πΎ =
βͺ ((π₯ β π΄ β¦ πΎ)βπ₯) β Xπ₯ β π΄ βͺ πΎ = Xπ₯ β π΄ βͺ ((π₯ β π΄ β¦ πΎ)βπ₯)) |
8 | 6, 7 | syl 17 |
. . 3
β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ₯ β
π΄ βͺ πΎ =
Xπ₯
β π΄ βͺ ((π₯
β π΄ β¦ πΎ)βπ₯)) |
9 | | nffvmpt1 6899 |
. . . . 5
β’
β²π₯((π₯ β π΄ β¦ πΎ)βπ¦) |
10 | 9 | nfuni 4914 |
. . . 4
β’
β²π₯βͺ ((π₯
β π΄ β¦ πΎ)βπ¦) |
11 | | nfcv 2903 |
. . . 4
β’
β²π¦βͺ ((π₯
β π΄ β¦ πΎ)βπ₯) |
12 | | fveq2 6888 |
. . . . 5
β’ (π¦ = π₯ β ((π₯ β π΄ β¦ πΎ)βπ¦) = ((π₯ β π΄ β¦ πΎ)βπ₯)) |
13 | 12 | unieqd 4921 |
. . . 4
β’ (π¦ = π₯ β βͺ ((π₯ β π΄ β¦ πΎ)βπ¦) = βͺ ((π₯ β π΄ β¦ πΎ)βπ₯)) |
14 | 10, 11, 13 | cbvixp 8904 |
. . 3
β’ Xπ¦ β
π΄ βͺ ((π₯
β π΄ β¦ πΎ)βπ¦) = Xπ₯ β π΄ βͺ ((π₯ β π΄ β¦ πΎ)βπ₯) |
15 | 8, 14 | eqtr4di 2790 |
. 2
β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ₯ β
π΄ βͺ πΎ =
Xπ¦
β π΄ βͺ ((π₯
β π΄ β¦ πΎ)βπ¦)) |
16 | 1 | fmpt 7106 |
. . 3
β’
(βπ₯ β
π΄ πΎ β Top β (π₯ β π΄ β¦ πΎ):π΄βΆTop) |
17 | | ptunimpt.j |
. . . 4
β’ π½ =
(βtβ(π₯ β π΄ β¦ πΎ)) |
18 | 17 | ptuni 23089 |
. . 3
β’ ((π΄ β π β§ (π₯ β π΄ β¦ πΎ):π΄βΆTop) β Xπ¦ β
π΄ βͺ ((π₯
β π΄ β¦ πΎ)βπ¦) = βͺ π½) |
19 | 16, 18 | sylan2b 594 |
. 2
β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ¦ β
π΄ βͺ ((π₯
β π΄ β¦ πΎ)βπ¦) = βͺ π½) |
20 | 15, 19 | eqtrd 2772 |
1
β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ₯ β
π΄ βͺ πΎ =
βͺ π½) |