Step | Hyp | Ref
| Expression |
1 | | ucnprima.4 |
. . . . 5
|
2 | | ucnprima.3 |
. . . . . . 7
Cnu |
3 | | ucnprima.1 |
. . . . . . . 8
UnifOn |
4 | | ucnprima.2 |
. . . . . . . 8
UnifOn |
5 | | isucn 22082 |
. . . . . . . 8
UnifOn UnifOn
Cnu
|
6 | 3, 4, 5 | syl2anc 693 |
. . . . . . 7
Cnu
|
7 | 2, 6 | mpbid 222 |
. . . . . 6
|
8 | 7 | simprd 479 |
. . . . 5
|
9 | | breq 4655 |
. . . . . . . . 9
|
10 | 9 | imbi2d 330 |
. . . . . . . 8
|
11 | 10 | ralbidv 2986 |
. . . . . . 7
|
12 | 11 | rexralbidv 3058 |
. . . . . 6
|
13 | 12 | rspcv 3305 |
. . . . 5
|
14 | 1, 8, 13 | sylc 65 |
. . . 4
|
15 | | simplll 798 |
. . . . . . . . 9
|
16 | | simplr 792 |
. . . . . . . . 9
|
17 | 15, 16 | jca 554 |
. . . . . . . 8
|
18 | | ustssxp 22008 |
. . . . . . . . . . 11
UnifOn |
19 | 3, 18 | sylan 488 |
. . . . . . . . . 10
|
20 | 19 | sselda 3603 |
. . . . . . . . 9
|
21 | 20 | adantlr 751 |
. . . . . . . 8
|
22 | | simpr 477 |
. . . . . . . 8
|
23 | | simplr 792 |
. . . . . . . . . . 11
|
24 | | simpr 477 |
. . . . . . . . . . . . . 14
|
25 | | elxp2 5132 |
. . . . . . . . . . . . . 14
|
26 | 24, 25 | sylib 208 |
. . . . . . . . . . . . 13
|
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 27 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
30 | | df-br 4654 |
. . . . . . . . . . . . . . . . . 18
|
31 | 29, 30 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
|
32 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | | ucnprima.5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
35 | 3, 4, 2, 1, 34 | ucnimalem 22084 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | 35 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | 32, 33, 36 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
39 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
40 | 32, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
41 | 38, 40 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
42 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | 42, 43 | opth 4945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | 41, 44 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 45 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | 48 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | 47, 49 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 37, 50 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
|
53 | | df-br 4654 |
. . . . . . . . . . . . . . . . . 18
|
54 | 52, 53 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
|
55 | 31, 54 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | exbiri 652 |
. . . . . . . . . . . . . . 15
|
57 | 56 | reximdv 3016 |
. . . . . . . . . . . . . 14
|
58 | 57 | reximdv 3016 |
. . . . . . . . . . . . 13
|
59 | 26, 58 | mpd 15 |
. . . . . . . . . . . 12
|
60 | 59 | adantlr 751 |
. . . . . . . . . . 11
|
61 | 23, 60 | r19.29d2r 3080 |
. . . . . . . . . 10
|
62 | | pm3.35 611 |
. . . . . . . . . . . 12
|
63 | 62 | rexlimivw 3029 |
. . . . . . . . . . 11
|
64 | 63 | rexlimivw 3029 |
. . . . . . . . . 10
|
65 | 61, 64 | syl 17 |
. . . . . . . . 9
|
66 | 65 | imp 445 |
. . . . . . . 8
|
67 | 17, 21, 22, 66 | syl21anc 1325 |
. . . . . . 7
|
68 | 67 | ralrimiva 2966 |
. . . . . 6
|
69 | 68 | ex 450 |
. . . . 5
|
70 | 69 | reximdva 3017 |
. . . 4
|
71 | 14, 70 | mpd 15 |
. . 3
|
72 | 34 | mpt2fun 6762 |
. . . . . 6
|
73 | | opex 4932 |
. . . . . . . 8
|
74 | 34, 73 | dmmpt2 7240 |
. . . . . . 7
|
75 | 19, 74 | syl6sseqr 3652 |
. . . . . 6
|
76 | | funimass4 6247 |
. . . . . 6
|
77 | 72, 75, 76 | sylancr 695 |
. . . . 5
|
78 | 77 | biimprd 238 |
. . . 4
|
79 | 78 | ralrimiva 2966 |
. . 3
|
80 | | r19.29r 3073 |
. . 3
|
81 | 71, 79, 80 | syl2anc 693 |
. 2
|
82 | | pm3.35 611 |
. . 3
|
83 | 82 | reximi 3011 |
. 2
|
84 | 81, 83 | syl 17 |
1
|