Step | Hyp | Ref
| Expression |
1 | | utoptop.1 |
. . . . . . . 8
β’ π½ = (unifTopβπ) |
2 | | utopval 23737 |
. . . . . . . 8
β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ β π βπ€ β π (π€ β {π}) β π}) |
3 | 1, 2 | eqtrid 2785 |
. . . . . . 7
β’ (π β (UnifOnβπ) β π½ = {π β π« π β£ βπ β π βπ€ β π (π€ β {π}) β π}) |
4 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β π β (UnifOnβπ)) |
5 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β (UnifOnβπ) β§ π β π« π) β π β π« π) |
6 | 5 | elpwid 4612 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π β π« π) β π β π) |
7 | 6 | sselda 3983 |
. . . . . . . . . . 11
β’ (((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β π β π) |
8 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β (UnifOnβπ) β§ π β π) β π β π) |
9 | | mptexg 7223 |
. . . . . . . . . . . . . . . 16
β’ (π β (UnifOnβπ) β (π£ β π β¦ (π£ β {π})) β V) |
10 | | rnexg 7895 |
. . . . . . . . . . . . . . . 16
β’ ((π£ β π β¦ (π£ β {π})) β V β ran (π£ β π β¦ (π£ β {π})) β V) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (UnifOnβπ) β ran (π£ β π β¦ (π£ β {π})) β V) |
12 | 11 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (UnifOnβπ) β§ π β π) β ran (π£ β π β¦ (π£ β {π})) β V) |
13 | | utopsnneip.2 |
. . . . . . . . . . . . . . 15
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
14 | 13 | fvmpt2 7010 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β (πβπ) = ran (π£ β π β¦ (π£ β {π}))) |
15 | 8, 12, 14 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β (UnifOnβπ) β§ π β π) β (πβπ) = ran (π£ β π β¦ (π£ β {π}))) |
16 | 15 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β π β ran (π£ β π β¦ (π£ β {π})))) |
17 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π})) |
18 | 17 | elrnmpt 5956 |
. . . . . . . . . . . . 13
β’ (π β V β (π β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π π = (π£ β {π}))) |
19 | 18 | elv 3481 |
. . . . . . . . . . . 12
β’ (π β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π π = (π£ β {π})) |
20 | 16, 19 | bitrdi 287 |
. . . . . . . . . . 11
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β βπ£ β π π = (π£ β {π}))) |
21 | 4, 7, 20 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β (π β (πβπ) β βπ£ β π π = (π£ β {π}))) |
22 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π£((π β (UnifOnβπ) β§ π β π« π) β§ π β π) |
23 | | nfre1 3283 |
. . . . . . . . . . . . 13
β’
β²π£βπ£ β π π = (π£ β {π}) |
24 | 22, 23 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π£(((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) |
25 | | simplr 768 |
. . . . . . . . . . . . 13
β’
((((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) β§ π£ β π) β§ π = (π£ β {π})) β π£ β π) |
26 | | eqimss2 4042 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β {π}) β (π£ β {π}) β π) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . 13
β’
((((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) β§ π£ β π) β§ π = (π£ β {π})) β (π£ β {π}) β π) |
28 | | imaeq1 6055 |
. . . . . . . . . . . . . . 15
β’ (π€ = π£ β (π€ β {π}) = (π£ β {π})) |
29 | 28 | sseq1d 4014 |
. . . . . . . . . . . . . 14
β’ (π€ = π£ β ((π€ β {π}) β π β (π£ β {π}) β π)) |
30 | 29 | rspcev 3613 |
. . . . . . . . . . . . 13
β’ ((π£ β π β§ (π£ β {π}) β π) β βπ€ β π (π€ β {π}) β π) |
31 | 25, 27, 30 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) β§ π£ β π) β§ π = (π£ β {π})) β βπ€ β π (π€ β {π}) β π) |
32 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) β βπ£ β π π = (π£ β {π})) |
33 | 24, 31, 32 | r19.29af 3266 |
. . . . . . . . . . 11
β’ ((((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β§ βπ£ β π π = (π£ β {π})) β βπ€ β π (π€ β {π}) β π) |
34 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β π β (UnifOnβπ)) |
35 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β π β π) |
36 | 34, 35 | jca 513 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β (π β (UnifOnβπ) β§ π β π)) |
37 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β (π€ β {π}) β π) |
38 | 6 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β π β π) |
39 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β π€ β π) |
40 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {π}) = (π€ β {π}) |
41 | | imaeq1 6055 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ = π€ β (π’ β {π}) = (π€ β {π})) |
42 | 41 | rspceeqv 3634 |
. . . . . . . . . . . . . . . . . 18
β’ ((π€ β π β§ (π€ β {π}) = (π€ β {π})) β βπ’ β π (π€ β {π}) = (π’ β {π})) |
43 | 40, 42 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β π β βπ’ β π (π€ β {π}) = (π’ β {π})) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β βπ’ β π (π€ β {π}) = (π’ β {π})) |
45 | | vex 3479 |
. . . . . . . . . . . . . . . . . . 19
β’ π€ β V |
46 | 45 | imaex 7907 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {π}) β V |
47 | 13 | ustuqtoplem 23744 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (UnifOnβπ) β§ π β π) β§ (π€ β {π}) β V) β ((π€ β {π}) β (πβπ) β βπ’ β π (π€ β {π}) = (π’ β {π}))) |
48 | 46, 47 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (UnifOnβπ) β§ π β π) β ((π€ β {π}) β (πβπ) β βπ’ β π (π€ β {π}) = (π’ β {π}))) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β ((π€ β {π}) β (πβπ) β βπ’ β π (π€ β {π}) = (π’ β {π}))) |
50 | 44, 49 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β (π€ β {π}) β (πβπ)) |
51 | 34, 35, 39, 50 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β (π€ β {π}) β (πβπ)) |
52 | | sseq1 4008 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π€ β {π}) β (π β π β (π€ β {π}) β π)) |
53 | 52 | 3anbi2d 1442 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π€ β {π}) β (((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β ((π β (UnifOnβπ) β§ π β π) β§ (π€ β {π}) β π β§ π β π))) |
54 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π€ β {π}) β (π β (πβπ) β (π€ β {π}) β (πβπ))) |
55 | 53, 54 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = (π€ β {π}) β ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β (((π β (UnifOnβπ) β§ π β π) β§ (π€ β {π}) β π β§ π β π) β§ (π€ β {π}) β (πβπ)))) |
56 | 55 | imbi1d 342 |
. . . . . . . . . . . . . . 15
β’ (π = (π€ β {π}) β (((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) β ((((π β (UnifOnβπ) β§ π β π) β§ (π€ β {π}) β π β§ π β π) β§ (π€ β {π}) β (πβπ)) β π β (πβπ)))) |
57 | 13 | ustuqtop1 23746 |
. . . . . . . . . . . . . . 15
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
58 | 46, 56, 57 | vtocl 3550 |
. . . . . . . . . . . . . 14
β’ ((((π β (UnifOnβπ) β§ π β π) β§ (π€ β {π}) β π β§ π β π) β§ (π€ β {π}) β (πβπ)) β π β (πβπ)) |
59 | 36, 37, 38, 51, 58 | syl31anc 1374 |
. . . . . . . . . . . . 13
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β π β (πβπ)) |
60 | 36, 20 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β (π β (πβπ) β βπ£ β π π = (π£ β {π}))) |
61 | 59, 60 | mpbid 231 |
. . . . . . . . . . . 12
β’
(((((π β
(UnifOnβπ) β§
π β π« π) β§ π β π) β§ π€ β π) β§ (π€ β {π}) β π) β βπ£ β π π = (π£ β {π})) |
62 | 61 | r19.29an 3159 |
. . . . . . . . . . 11
β’ ((((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β§ βπ€ β π (π€ β {π}) β π) β βπ£ β π π = (π£ β {π})) |
63 | 33, 62 | impbida 800 |
. . . . . . . . . 10
β’ (((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β (βπ£ β π π = (π£ β {π}) β βπ€ β π (π€ β {π}) β π)) |
64 | 21, 63 | bitrd 279 |
. . . . . . . . 9
β’ (((π β (UnifOnβπ) β§ π β π« π) β§ π β π) β (π β (πβπ) β βπ€ β π (π€ β {π}) β π)) |
65 | 64 | ralbidva 3176 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π β π« π) β (βπ β π π β (πβπ) β βπ β π βπ€ β π (π€ β {π}) β π)) |
66 | 65 | rabbidva 3440 |
. . . . . . 7
β’ (π β (UnifOnβπ) β {π β π« π β£ βπ β π π β (πβπ)} = {π β π« π β£ βπ β π βπ€ β π (π€ β {π}) β π}) |
67 | 3, 66 | eqtr4d 2776 |
. . . . . 6
β’ (π β (UnifOnβπ) β π½ = {π β π« π β£ βπ β π π β (πβπ)}) |
68 | | utopsnneip.1 |
. . . . . 6
β’ πΎ = {π β π« π β£ βπ β π π β (πβπ)} |
69 | 67, 68 | eqtr4di 2791 |
. . . . 5
β’ (π β (UnifOnβπ) β π½ = πΎ) |
70 | 69 | fveq2d 6896 |
. . . 4
β’ (π β (UnifOnβπ) β (neiβπ½) = (neiβπΎ)) |
71 | 70 | fveq1d 6894 |
. . 3
β’ (π β (UnifOnβπ) β ((neiβπ½)β{π}) = ((neiβπΎ)β{π})) |
72 | 71 | adantr 482 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπ½)β{π}) = ((neiβπΎ)β{π})) |
73 | 13 | ustuqtop0 23745 |
. . . . 5
β’ (π β (UnifOnβπ) β π:πβΆπ« π« π) |
74 | 13 | ustuqtop1 23746 |
. . . . 5
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
75 | 13 | ustuqtop2 23747 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β (fiβ(πβπ)) β (πβπ)) |
76 | 13 | ustuqtop3 23748 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) |
77 | 13 | ustuqtop4 23749 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) |
78 | 13 | ustuqtop5 23750 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β π β (πβπ)) |
79 | 68, 73, 74, 75, 76, 77, 78 | neiptopnei 22636 |
. . . 4
β’ (π β (UnifOnβπ) β π = (π β π β¦ ((neiβπΎ)β{π}))) |
80 | 79 | adantr 482 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β π = (π β π β¦ ((neiβπΎ)β{π}))) |
81 | | simpr 486 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π = π) β π = π) |
82 | 81 | sneqd 4641 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β π) β§ π = π) β {π} = {π}) |
83 | 82 | fveq2d 6896 |
. . 3
β’ (((π β (UnifOnβπ) β§ π β π) β§ π = π) β ((neiβπΎ)β{π}) = ((neiβπΎ)β{π})) |
84 | | simpr 486 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β π β π) |
85 | | fvexd 6907 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπΎ)β{π}) β V) |
86 | 80, 83, 84, 85 | fvmptd 7006 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β (πβπ) = ((neiβπΎ)β{π})) |
87 | | mptexg 7223 |
. . . . 5
β’ (π β (UnifOnβπ) β (π£ β π β¦ (π£ β {π})) β V) |
88 | | rnexg 7895 |
. . . . 5
β’ ((π£ β π β¦ (π£ β {π})) β V β ran (π£ β π β¦ (π£ β {π})) β V) |
89 | 87, 88 | syl 17 |
. . . 4
β’ (π β (UnifOnβπ) β ran (π£ β π β¦ (π£ β {π})) β V) |
90 | 89 | adantr 482 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β ran (π£ β π β¦ (π£ β {π})) β V) |
91 | | nfv 1918 |
. . . . . . . 8
β’
β²π£ π β π |
92 | | nfmpt1 5257 |
. . . . . . . . . 10
β’
β²π£(π£ β π β¦ (π£ β {π})) |
93 | 92 | nfrn 5952 |
. . . . . . . . 9
β’
β²π£ran
(π£ β π β¦ (π£ β {π})) |
94 | 93 | nfel1 2920 |
. . . . . . . 8
β’
β²π£ran (π£ β π β¦ (π£ β {π})) β V |
95 | 91, 94 | nfan 1903 |
. . . . . . 7
β’
β²π£(π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) |
96 | | nfv 1918 |
. . . . . . 7
β’
β²π£ π = π |
97 | 95, 96 | nfan 1903 |
. . . . . 6
β’
β²π£((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β§ π = π) |
98 | | simpr2 1196 |
. . . . . . . . 9
β’ ((π β π β§ (ran (π£ β π β¦ (π£ β {π})) β V β§ π = π β§ π£ β π)) β π = π) |
99 | 98 | sneqd 4641 |
. . . . . . . 8
β’ ((π β π β§ (ran (π£ β π β¦ (π£ β {π})) β V β§ π = π β§ π£ β π)) β {π} = {π}) |
100 | 99 | imaeq2d 6060 |
. . . . . . 7
β’ ((π β π β§ (ran (π£ β π β¦ (π£ β {π})) β V β§ π = π β§ π£ β π)) β (π£ β {π}) = (π£ β {π})) |
101 | 100 | 3anassrs 1361 |
. . . . . 6
β’ ((((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β§ π = π) β§ π£ β π) β (π£ β {π}) = (π£ β {π})) |
102 | 97, 101 | mpteq2da 5247 |
. . . . 5
β’ (((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β§ π = π) β (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π}))) |
103 | 102 | rneqd 5938 |
. . . 4
β’ (((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β§ π = π) β ran (π£ β π β¦ (π£ β {π})) = ran (π£ β π β¦ (π£ β {π}))) |
104 | | simpl 484 |
. . . 4
β’ ((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β π β π) |
105 | | simpr 486 |
. . . 4
β’ ((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β ran (π£ β π β¦ (π£ β {π})) β V) |
106 | 13, 103, 104, 105 | fvmptd2 7007 |
. . 3
β’ ((π β π β§ ran (π£ β π β¦ (π£ β {π})) β V) β (πβπ) = ran (π£ β π β¦ (π£ β {π}))) |
107 | 84, 90, 106 | syl2anc 585 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π) β (πβπ) = ran (π£ β π β¦ (π£ β {π}))) |
108 | 72, 86, 107 | 3eqtr2d 2779 |
1
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπ½)β{π}) = ran (π£ β π β¦ (π£ β {π}))) |