Step | Hyp | Ref
| Expression |
1 | | elfvunirn 6857 |
. . . 4
β’ (π β (UnifOnβπ) β π β βͺ ran
UnifOn) |
2 | 1 | adantr 481 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β π β βͺ ran
UnifOn) |
3 | | elfvunirn 6857 |
. . . 4
β’ (π β (UnifOnβπ) β π β βͺ ran
UnifOn) |
4 | 3 | adantl 482 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β π β βͺ ran
UnifOn) |
5 | | ovex 7370 |
. . . . 5
β’ (dom
βͺ π βm dom βͺ π)
β V |
6 | 5 | rabex 5276 |
. . . 4
β’ {π β (dom βͺ π
βm dom βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))} β V |
7 | 6 | a1i 11 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β {π β (dom βͺ
π βm dom
βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))} β V) |
8 | | simpr 485 |
. . . . . . . 8
β’ ((π’ = π β§ π£ = π) β π£ = π) |
9 | 8 | unieqd 4866 |
. . . . . . 7
β’ ((π’ = π β§ π£ = π) β βͺ π£ = βͺ
π) |
10 | 9 | dmeqd 5847 |
. . . . . 6
β’ ((π’ = π β§ π£ = π) β dom βͺ
π£ = dom βͺ π) |
11 | | simpl 483 |
. . . . . . . 8
β’ ((π’ = π β§ π£ = π) β π’ = π) |
12 | 11 | unieqd 4866 |
. . . . . . 7
β’ ((π’ = π β§ π£ = π) β βͺ π’ = βͺ
π) |
13 | 12 | dmeqd 5847 |
. . . . . 6
β’ ((π’ = π β§ π£ = π) β dom βͺ
π’ = dom βͺ π) |
14 | 10, 13 | oveq12d 7355 |
. . . . 5
β’ ((π’ = π β§ π£ = π) β (dom βͺ
π£ βm dom
βͺ π’) = (dom βͺ π βm dom βͺ π)) |
15 | 13 | raleqdv 3309 |
. . . . . . . 8
β’ ((π’ = π β§ π£ = π) β (βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
16 | 13, 15 | raleqbidv 3315 |
. . . . . . 7
β’ ((π’ = π β§ π£ = π) β (βπ₯ β dom βͺ
π’βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
17 | 11, 16 | rexeqbidv 3316 |
. . . . . 6
β’ ((π’ = π β§ π£ = π) β (βπ β π’ βπ₯ β dom βͺ
π’βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
18 | 8, 17 | raleqbidv 3315 |
. . . . 5
β’ ((π’ = π β§ π£ = π) β (βπ β π£ βπ β π’ βπ₯ β dom βͺ
π’βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
19 | 14, 18 | rabeqbidv 3420 |
. . . 4
β’ ((π’ = π β§ π£ = π) β {π β (dom βͺ
π£ βm dom
βͺ π’) β£ βπ β π£ βπ β π’ βπ₯ β dom βͺ
π’βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦))} = {π β (dom βͺ
π βm dom
βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |
20 | | df-ucn 23534 |
. . . 4
β’
Cnu = (π’ β
βͺ ran UnifOn, π£ β βͺ ran
UnifOn β¦ {π β
(dom βͺ π£ βm dom βͺ π’)
β£ βπ β
π£ βπ β π’ βπ₯ β dom βͺ
π’βπ¦ β dom βͺ
π’(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |
21 | 19, 20 | ovmpoga 7489 |
. . 3
β’ ((π β βͺ ran UnifOn β§ π β βͺ ran
UnifOn β§ {π β (dom
βͺ π βm dom βͺ π)
β£ βπ β
π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))} β V) β (π Cnuπ) = {π β (dom βͺ
π βm dom
βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |
22 | 2, 4, 7, 21 | syl3anc 1370 |
. 2
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (π Cnuπ) = {π β (dom βͺ
π βm dom
βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |
23 | | ustbas2 23483 |
. . . 4
β’ (π β (UnifOnβπ) β π = dom βͺ π) |
24 | | ustbas2 23483 |
. . . 4
β’ (π β (UnifOnβπ) β π = dom βͺ π) |
25 | 23, 24 | oveqan12rd 7357 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (π βm π) = (dom βͺ π βm dom βͺ π)) |
26 | 24 | adantr 481 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β π = dom βͺ π) |
27 | 26 | raleqdv 3309 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
28 | 26, 27 | raleqbidv 3315 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
29 | 28 | rexbidv 3171 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
30 | 29 | ralbidv 3170 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (βπ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦)) β βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦)))) |
31 | 25, 30 | rabeqbidv 3420 |
. 2
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β {π β (π βm π) β£ βπ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦))} = {π β (dom βͺ
π βm dom
βͺ π) β£ βπ β π βπ β π βπ₯ β dom βͺ
πβπ¦ β dom βͺ
π(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |
32 | 22, 31 | eqtr4d 2779 |
1
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (π Cnuπ) = {π β (π βm π) β£ βπ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦))}) |