Step | Hyp | Ref
| Expression |
1 | | simplll 773 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β (π β (UnifOnβπ) β§ π β π)) |
2 | | simplr 767 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β π’ β π) |
3 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π’ β {π}) = (π’ β {π}) |
4 | | imaeq1 6054 |
. . . . . . . . . . . 12
β’ (π€ = π’ β (π€ β {π}) = (π’ β {π})) |
5 | 4 | rspceeqv 3633 |
. . . . . . . . . . 11
β’ ((π’ β π β§ (π’ β {π}) = (π’ β {π})) β βπ€ β π (π’ β {π}) = (π€ β {π})) |
6 | 3, 5 | mpan2 689 |
. . . . . . . . . 10
β’ (π’ β π β βπ€ β π (π’ β {π}) = (π€ β {π})) |
7 | 6 | adantl 482 |
. . . . . . . . 9
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β βπ€ β π (π’ β {π}) = (π€ β {π})) |
8 | | imaexg 7908 |
. . . . . . . . . 10
β’ (π’ β π β (π’ β {π}) β V) |
9 | | utopustuq.1 |
. . . . . . . . . . 11
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
10 | 9 | ustuqtoplem 23751 |
. . . . . . . . . 10
β’ (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β V) β ((π’ β {π}) β (πβπ) β βπ€ β π (π’ β {π}) = (π€ β {π}))) |
11 | 8, 10 | sylan2 593 |
. . . . . . . . 9
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β ((π’ β {π}) β (πβπ) β βπ€ β π (π’ β {π}) = (π€ β {π}))) |
12 | 7, 11 | mpbird 256 |
. . . . . . . 8
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β (π’ β {π}) β (πβπ)) |
13 | 1, 2, 12 | syl2anc 584 |
. . . . . . 7
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β (π’ β {π}) β (πβπ)) |
14 | | simp-5l 783 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β π β (UnifOnβπ)) |
15 | 1 | simpld 495 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β π β (UnifOnβπ)) |
16 | | simp-4r 782 |
. . . . . . . . . . . . . 14
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β π β π) |
17 | | ustimasn 23740 |
. . . . . . . . . . . . . 14
β’ ((π β (UnifOnβπ) β§ π’ β π β§ π β π) β (π’ β {π}) β π) |
18 | 15, 2, 16, 17 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β (π’ β {π}) β π) |
19 | 18 | sselda 3982 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β π β π) |
20 | 14, 19 | jca 512 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π β (UnifOnβπ) β§ π β π)) |
21 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π β (π’ β {π})) |
22 | | simp-6l 785 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π β (UnifOnβπ)) |
23 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π’ β π) |
24 | | ustrel 23723 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (UnifOnβπ) β§ π’ β π) β Rel π’) |
25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β Rel π’) |
26 | | elrelimasn 6084 |
. . . . . . . . . . . . . . . . . 18
β’ (Rel
π’ β (π β (π’ β {π}) β ππ’π)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β (π β (π’ β {π}) β ππ’π)) |
28 | 21, 27 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β ππ’π) |
29 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π β (π’ β {π})) |
30 | | elrelimasn 6084 |
. . . . . . . . . . . . . . . . . 18
β’ (Rel
π’ β (π β (π’ β {π}) β ππ’π)) |
31 | 25, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β (π β (π’ β {π}) β ππ’π)) |
32 | 29, 31 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β ππ’π) |
33 | | vex 3478 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
34 | | vex 3478 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
35 | 33, 34 | brco 5870 |
. . . . . . . . . . . . . . . . . 18
β’ (π(π’ β π’)π β βπ(ππ’π β§ ππ’π)) |
36 | 35 | biimpri 227 |
. . . . . . . . . . . . . . . . 17
β’
(βπ(ππ’π β§ ππ’π) β π(π’ β π’)π) |
37 | 36 | 19.23bi 2184 |
. . . . . . . . . . . . . . . 16
β’ ((ππ’π β§ ππ’π) β π(π’ β π’)π) |
38 | 28, 32, 37 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π(π’ β π’)π) |
39 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β (π’ β π’) β π€) |
40 | 39 | ssbrd 5191 |
. . . . . . . . . . . . . . 15
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β (π(π’ β π’)π β ππ€π)) |
41 | 38, 40 | mpd 15 |
. . . . . . . . . . . . . 14
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β ππ€π) |
42 | | simp-5r 784 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π€ β π) |
43 | | ustrel 23723 |
. . . . . . . . . . . . . . . 16
β’ ((π β (UnifOnβπ) β§ π€ β π) β Rel π€) |
44 | 22, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β Rel π€) |
45 | | elrelimasn 6084 |
. . . . . . . . . . . . . . 15
β’ (Rel
π€ β (π β (π€ β {π}) β ππ€π)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β (π β (π€ β {π}) β ππ€π)) |
47 | 41, 46 | mpbird 256 |
. . . . . . . . . . . . 13
β’
(((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β§ π β (π’ β {π})) β π β (π€ β {π})) |
48 | 47 | ex 413 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π β (π’ β {π}) β π β (π€ β {π}))) |
49 | 48 | ssrdv 3988 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π’ β {π}) β (π€ β {π})) |
50 | | simp-4r 782 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β π€ β π) |
51 | 16 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β π β π) |
52 | | ustimasn 23740 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π€ β π β§ π β π) β (π€ β {π}) β π) |
53 | 14, 50, 51, 52 | syl3anc 1371 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π€ β {π}) β π) |
54 | 20, 49, 53 | 3jca 1128 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β ((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π)) |
55 | | simpllr 774 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β π’ β π) |
56 | | eqidd 2733 |
. . . . . . . . . . . . . 14
β’ (π’ β π β (π’ β {π}) = (π’ β {π})) |
57 | | imaeq1 6054 |
. . . . . . . . . . . . . . 15
β’ (π€ = π’ β (π€ β {π}) = (π’ β {π})) |
58 | 57 | rspceeqv 3633 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ (π’ β {π}) = (π’ β {π})) β βπ€ β π (π’ β {π}) = (π€ β {π})) |
59 | 56, 58 | mpdan 685 |
. . . . . . . . . . . . 13
β’ (π’ β π β βπ€ β π (π’ β {π}) = (π€ β {π})) |
60 | 59 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β βπ€ β π (π’ β {π}) = (π€ β {π})) |
61 | | imaexg 7908 |
. . . . . . . . . . . . 13
β’ (π’ β π β (π’ β {π}) β V) |
62 | 9 | ustuqtoplem 23751 |
. . . . . . . . . . . . 13
β’ (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β V) β ((π’ β {π}) β (πβπ) β βπ€ β π (π’ β {π}) = (π€ β {π}))) |
63 | 61, 62 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β ((π’ β {π}) β (πβπ) β βπ€ β π (π’ β {π}) = (π€ β {π}))) |
64 | 60, 63 | mpbird 256 |
. . . . . . . . . . 11
β’ (((π β (UnifOnβπ) β§ π β π) β§ π’ β π) β (π’ β {π}) β (πβπ)) |
65 | 14, 19, 55, 64 | syl21anc 836 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π’ β {π}) β (πβπ)) |
66 | 54, 65 | jca 512 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ))) |
67 | | imaexg 7908 |
. . . . . . . . . . 11
β’ (π€ β π β (π€ β {π}) β V) |
68 | | sseq2 4008 |
. . . . . . . . . . . . . . . 16
β’ (π = (π€ β {π}) β ((π’ β {π}) β π β (π’ β {π}) β (π€ β {π}))) |
69 | | sseq1 4007 |
. . . . . . . . . . . . . . . 16
β’ (π = (π€ β {π}) β (π β π β (π€ β {π}) β π)) |
70 | 68, 69 | 3anbi23d 1439 |
. . . . . . . . . . . . . . 15
β’ (π = (π€ β {π}) β (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β ((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π))) |
71 | 70 | anbi1d 630 |
. . . . . . . . . . . . . 14
β’ (π = (π€ β {π}) β ((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)))) |
72 | 71 | anbi1d 630 |
. . . . . . . . . . . . 13
β’ (π = (π€ β {π}) β (((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β ((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π))) |
73 | | eleq1 2821 |
. . . . . . . . . . . . 13
β’ (π = (π€ β {π}) β (π β (πβπ) β (π€ β {π}) β (πβπ))) |
74 | 72, 73 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π = (π€ β {π}) β ((((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β π β (πβπ)) β (((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β (π€ β {π}) β (πβπ)))) |
75 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π’ β {π}) β (π β π β (π’ β {π}) β π)) |
76 | 75 | 3anbi2d 1441 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π’ β {π}) β (((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β ((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π))) |
77 | | eleq1 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π’ β {π}) β (π β (πβπ) β (π’ β {π}) β (πβπ))) |
78 | 76, 77 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = (π’ β {π}) β ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β (((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)))) |
79 | 78 | imbi1d 341 |
. . . . . . . . . . . . . . 15
β’ (π = (π’ β {π}) β (((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) β ((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β π β (πβπ)))) |
80 | | eleq1 2821 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β π β π β π)) |
81 | 80 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π β (UnifOnβπ) β§ π β π) β (π β (UnifOnβπ) β§ π β π))) |
82 | 81 | 3anbi1d 1440 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β ((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π))) |
83 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πβπ) = (πβπ)) |
84 | 83 | eleq2d 2819 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
85 | 82, 84 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β (((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)))) |
86 | 83 | eleq2d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
87 | 85, 86 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) β ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)))) |
88 | 9 | ustuqtop1 23753 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
89 | 87, 88 | chvarvv 2002 |
. . . . . . . . . . . . . . 15
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
90 | 79, 89 | vtoclg 3556 |
. . . . . . . . . . . . . 14
β’ ((π’ β {π}) β V β ((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β π β (πβπ))) |
91 | 61, 90 | syl 17 |
. . . . . . . . . . . . 13
β’ (π’ β π β ((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β π β (πβπ))) |
92 | 91 | impcom 408 |
. . . . . . . . . . . 12
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ (π’ β {π}) β π β§ π β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β π β (πβπ)) |
93 | 74, 92 | vtoclg 3556 |
. . . . . . . . . . 11
β’ ((π€ β {π}) β V β (((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β (π€ β {π}) β (πβπ))) |
94 | 67, 93 | syl 17 |
. . . . . . . . . 10
β’ (π€ β π β (((((π β (UnifOnβπ) β§ π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β (π€ β {π}) β (πβπ))) |
95 | 94 | impcom 408 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ (π’ β {π}) β (π€ β {π}) β§ (π€ β {π}) β π) β§ (π’ β {π}) β (πβπ)) β§ π’ β π) β§ π€ β π) β (π€ β {π}) β (πβπ)) |
96 | 66, 55, 50, 95 | syl21anc 836 |
. . . . . . . 8
β’
((((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β§ π β (π’ β {π})) β (π€ β {π}) β (πβπ)) |
97 | 96 | ralrimiva 3146 |
. . . . . . 7
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β βπ β (π’ β {π})(π€ β {π}) β (πβπ)) |
98 | | raleq 3322 |
. . . . . . . 8
β’ (π = (π’ β {π}) β (βπ β π (π€ β {π}) β (πβπ) β βπ β (π’ β {π})(π€ β {π}) β (πβπ))) |
99 | 98 | rspcev 3612 |
. . . . . . 7
β’ (((π’ β {π}) β (πβπ) β§ βπ β (π’ β {π})(π€ β {π}) β (πβπ)) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ)) |
100 | 13, 97, 99 | syl2anc 584 |
. . . . . 6
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π€ β π) β§ π’ β π) β§ (π’ β π’) β π€) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ)) |
101 | | ustexhalf 23722 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π€ β π) β βπ’ β π (π’ β π’) β π€) |
102 | 101 | adantlr 713 |
. . . . . 6
β’ (((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β βπ’ β π (π’ β π’) β π€) |
103 | 100, 102 | r19.29a 3162 |
. . . . 5
β’ (((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ)) |
104 | 103 | adantr 481 |
. . . 4
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β§ π = (π€ β {π})) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ)) |
105 | | eleq1 2821 |
. . . . . 6
β’ (π = (π€ β {π}) β (π β (πβπ) β (π€ β {π}) β (πβπ))) |
106 | 105 | rexralbidv 3220 |
. . . . 5
β’ (π = (π€ β {π}) β (βπ β (πβπ)βπ β π π β (πβπ) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ))) |
107 | 106 | adantl 482 |
. . . 4
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β§ π = (π€ β {π})) β (βπ β (πβπ)βπ β π π β (πβπ) β βπ β (πβπ)βπ β π (π€ β {π}) β (πβπ))) |
108 | 104, 107 | mpbird 256 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π€ β π) β§ π = (π€ β {π})) β βπ β (πβπ)βπ β π π β (πβπ)) |
109 | 108 | adantllr 717 |
. 2
β’
(((((π β
(UnifOnβπ) β§
π β π) β§ π β (πβπ)) β§ π€ β π) β§ π = (π€ β {π})) β βπ β (πβπ)βπ β π π β (πβπ)) |
110 | | vex 3478 |
. . . 4
β’ π β V |
111 | 9 | ustuqtoplem 23751 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β V) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
112 | 110, 111 | mpan2 689 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (π β (πβπ) β βπ€ β π π = (π€ β {π}))) |
113 | 112 | biimpa 477 |
. 2
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ€ β π π = (π€ β {π})) |
114 | 109, 113 | r19.29a 3162 |
1
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) |