Step | Hyp | Ref
| Expression |
1 | | utopustuq.1 |
. . . . 5
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
2 | | simpl 483 |
. . . . . . . . . 10
β’ ((π = π β§ π£ β π) β π = π) |
3 | 2 | sneqd 4640 |
. . . . . . . . 9
β’ ((π = π β§ π£ β π) β {π} = {π}) |
4 | 3 | imaeq2d 6059 |
. . . . . . . 8
β’ ((π = π β§ π£ β π) β (π£ β {π}) = (π£ β {π})) |
5 | 4 | mpteq2dva 5248 |
. . . . . . 7
β’ (π = π β (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π}))) |
6 | 5 | rneqd 5937 |
. . . . . 6
β’ (π = π β ran (π£ β π β¦ (π£ β {π})) = ran (π£ β π β¦ (π£ β {π}))) |
7 | 6 | cbvmptv 5261 |
. . . . 5
β’ (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
8 | 1, 7 | eqtri 2760 |
. . . 4
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
9 | | simpr2 1195 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ (π β π β§ π = π β§ π£ β π)) β π = π) |
10 | 9 | sneqd 4640 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ (π β π β§ π = π β§ π£ β π)) β {π} = {π}) |
11 | 10 | imaeq2d 6059 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ (π β π β§ π = π β§ π£ β π)) β (π£ β {π}) = (π£ β {π})) |
12 | 11 | 3anassrs 1360 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π = π) β§ π£ β π) β (π£ β {π}) = (π£ β {π})) |
13 | 12 | mpteq2dva 5248 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π = π) β (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π}))) |
14 | 13 | rneqd 5937 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β π) β§ π = π) β ran (π£ β π β¦ (π£ β {π})) = ran (π£ β π β¦ (π£ β {π}))) |
15 | | simpr 485 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β π β π) |
16 | | mptexg 7225 |
. . . . . 6
β’ (π β (UnifOnβπ) β (π£ β π β¦ (π£ β {π})) β V) |
17 | | rnexg 7897 |
. . . . . 6
β’ ((π£ β π β¦ (π£ β {π})) β V β ran (π£ β π β¦ (π£ β {π})) β V) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (π β (UnifOnβπ) β ran (π£ β π β¦ (π£ β {π})) β V) |
19 | 18 | adantr 481 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β ran (π£ β π β¦ (π£ β {π})) β V) |
20 | 8, 14, 15, 19 | fvmptd2 7006 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (πβπ) = ran (π£ β π β¦ (π£ β {π}))) |
21 | 20 | eleq2d 2819 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β (π΄ β (πβπ) β π΄ β ran (π£ β π β¦ (π£ β {π})))) |
22 | | imaeq1 6054 |
. . . 4
β’ (π£ = π€ β (π£ β {π}) = (π€ β {π})) |
23 | 22 | cbvmptv 5261 |
. . 3
β’ (π£ β π β¦ (π£ β {π})) = (π€ β π β¦ (π€ β {π})) |
24 | 23 | elrnmpt 5955 |
. 2
β’ (π΄ β π β (π΄ β ran (π£ β π β¦ (π£ β {π})) β βπ€ β π π΄ = (π€ β {π}))) |
25 | 21, 24 | sylan9bb 510 |
1
β’ (((π β (UnifOnβπ) β§ π β π) β§ π΄ β π) β (π΄ β (πβπ) β βπ€ β π π΄ = (π€ β {π}))) |