Step | Hyp | Ref
| Expression |
1 | | ssun1 4133 |
. . . 4
β’ π β (π βͺ (π β π)) |
2 | | coires1 6217 |
. . . . . 6
β’ (π β ( I βΎ π)) = (π βΎ π) |
3 | | ustrel 23579 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) |
4 | | ustssxp 23572 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π Γ π)) |
5 | | dmss 5859 |
. . . . . . . . 9
β’ (π β (π Γ π) β dom π β dom (π Γ π)) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π β π) β dom π β dom (π Γ π)) |
7 | | dmxpid 5886 |
. . . . . . . 8
β’ dom
(π Γ π) = π |
8 | 6, 7 | sseqtrdi 3995 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π β π) β dom π β π) |
9 | | relssres 5979 |
. . . . . . 7
β’ ((Rel
π β§ dom π β π) β (π βΎ π) = π) |
10 | 3, 8, 9 | syl2anc 585 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β π) β (π βΎ π) = π) |
11 | 2, 10 | eqtrid 2785 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β (π β ( I βΎ π)) = π) |
12 | 11 | uneq1d 4123 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β ((π β ( I βΎ π)) βͺ (π β π)) = (π βͺ (π β π))) |
13 | 1, 12 | sseqtrrid 3998 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β π β ((π β ( I βΎ π)) βͺ (π β π))) |
14 | | coundi 6200 |
. . 3
β’ (π β (( I βΎ π) βͺ π)) = ((π β ( I βΎ π)) βͺ (π β π)) |
15 | 13, 14 | sseqtrrdi 3996 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β (( I βΎ π) βͺ π))) |
16 | | ustdiag 23576 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π) β ( I βΎ π) β π) |
17 | | ssequn1 4141 |
. . . 4
β’ (( I
βΎ π) β π β (( I βΎ π) βͺ π) = π) |
18 | 16, 17 | sylib 217 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (( I βΎ π) βͺ π) = π) |
19 | 18 | coeq2d 5819 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (( I βΎ π) βͺ π)) = (π β π)) |
20 | 15, 19 | sseqtrd 3985 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) |