Step | Hyp | Ref
| Expression |
1 | | ssun1 4167 |
. . . 4
β’ π β (π βͺ (π β π)) |
2 | | coires1 6256 |
. . . . . 6
β’ (π β ( I βΎ π)) = (π βΎ π) |
3 | | ustrel 24066 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) |
4 | | ustssxp 24059 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π Γ π)) |
5 | | dmss 5895 |
. . . . . . . . 9
β’ (π β (π Γ π) β dom π β dom (π Γ π)) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π β π) β dom π β dom (π Γ π)) |
7 | | dmxpid 5922 |
. . . . . . . 8
β’ dom
(π Γ π) = π |
8 | 6, 7 | sseqtrdi 4027 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π β π) β dom π β π) |
9 | | relssres 6015 |
. . . . . . 7
β’ ((Rel
π β§ dom π β π) β (π βΎ π) = π) |
10 | 3, 8, 9 | syl2anc 583 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β π) β (π βΎ π) = π) |
11 | 2, 10 | eqtrid 2778 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β (π β ( I βΎ π)) = π) |
12 | 11 | uneq1d 4157 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β ((π β ( I βΎ π)) βͺ (π β π)) = (π βͺ (π β π))) |
13 | 1, 12 | sseqtrrid 4030 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β π β ((π β ( I βΎ π)) βͺ (π β π))) |
14 | | coundi 6239 |
. . 3
β’ (π β (( I βΎ π) βͺ π)) = ((π β ( I βΎ π)) βͺ (π β π)) |
15 | 13, 14 | sseqtrrdi 4028 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β (( I βΎ π) βͺ π))) |
16 | | ustdiag 24063 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β ( I βΎ π) β π) |
17 | | ssequn1 4175 |
. . . 4
β’ (( I
βΎ π) β π β (( I βΎ π) βͺ π) = π) |
18 | 16, 17 | sylib 217 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (( I βΎ π) βͺ π) = π) |
19 | 18 | coeq2d 5855 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (( I βΎ π) βͺ π)) = (π β π)) |
20 | 15, 19 | sseqtrd 4017 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) |