Step | Hyp | Ref
| Expression |
1 | | fnresi 6679 |
. . . . . . 7
β’ ( I
βΎ π) Fn π |
2 | | fnsnfv 6970 |
. . . . . . 7
β’ ((( I
βΎ π) Fn π β§ π β π) β {(( I βΎ π)βπ)} = (( I βΎ π) β {π})) |
3 | 1, 2 | mpan 688 |
. . . . . 6
β’ (π β π β {(( I βΎ π)βπ)} = (( I βΎ π) β {π})) |
4 | 3 | ad4antlr 731 |
. . . . 5
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β {(( I βΎ π)βπ)} = (( I βΎ π) β {π})) |
5 | | ustdiag 23720 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π€ β π) β ( I βΎ π) β π€) |
6 | 5 | ad5ant14 756 |
. . . . . 6
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β ( I βΎ π) β π€) |
7 | | imass1 6100 |
. . . . . 6
β’ (( I
βΎ π) β π€ β (( I βΎ π) β {π}) β (π€ β {π})) |
8 | 6, 7 | syl 17 |
. . . . 5
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β (( I βΎ π) β {π}) β (π€ β {π})) |
9 | 4, 8 | eqsstrd 4020 |
. . . 4
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β {(( I βΎ π)βπ)} β (π€ β {π})) |
10 | | fvex 6904 |
. . . . 5
β’ (( I
βΎ π)βπ) β V |
11 | 10 | snss 4789 |
. . . 4
β’ ((( I
βΎ π)βπ) β (π€ β {π}) β {(( I βΎ π)βπ)} β (π€ β {π})) |
12 | 9, 11 | sylibr 233 |
. . 3
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β (( I βΎ π)βπ) β (π€ β {π})) |
13 | | fvresi 7173 |
. . . . 5
β’ (π β π β (( I βΎ π)βπ) = π) |
14 | 13 | eqcomd 2738 |
. . . 4
β’ (π β π β π = (( I βΎ π)βπ)) |
15 | 14 | ad4antlr 731 |
. . 3
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π = (( I βΎ π)βπ)) |
16 | | simpr 485 |
. . 3
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π = (π€ β {π})) |
17 | 12, 15, 16 | 3eltr4d 2848 |
. 2
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β π β π) |
18 | | utopustuq.1 |
. . . . 5
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
19 | 18 | ustuqtoplem 23751 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β V) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
20 | 19 | elvd 3481 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
21 | 20 | biimpa 477 |
. 2
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ€ β π π = (π€ β {π})) |
22 | 17, 21 | r19.29a 3162 |
1
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) |