Step |
Hyp |
Ref |
Expression |
1 |
|
pimdecfgtioc.x |
|- F/ x ph |
2 |
|
pimdecfgtioc.a |
|- ( ph -> A C_ RR ) |
3 |
|
pimdecfgtioc.f |
|- ( ph -> F : A --> RR* ) |
4 |
|
pimdecfgtioc.i |
|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) |
5 |
|
pimdecfgtioc.r |
|- ( ph -> R e. RR* ) |
6 |
|
pimdecfgtioc.y |
|- Y = { x e. A | R < ( F ` x ) } |
7 |
|
pimdecfgtioc.c |
|- S = sup ( Y , RR* , < ) |
8 |
|
pimdecfgtioc.e |
|- ( ph -> S e. Y ) |
9 |
|
pimdecfgtioc.d |
|- I = ( -oo (,] S ) |
10 |
|
ssrab2 |
|- { x e. A | R < ( F ` x ) } C_ A |
11 |
6 10
|
eqsstri |
|- Y C_ A |
12 |
11
|
a1i |
|- ( ph -> Y C_ A ) |
13 |
12 2
|
sstrd |
|- ( ph -> Y C_ RR ) |
14 |
13 7 8 9
|
ressiocsup |
|- ( ph -> Y C_ I ) |
15 |
14 12
|
ssind |
|- ( ph -> Y C_ ( I i^i A ) ) |
16 |
|
elinel2 |
|- ( x e. ( I i^i A ) -> x e. A ) |
17 |
16
|
adantl |
|- ( ( ph /\ x e. ( I i^i A ) ) -> x e. A ) |
18 |
5
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> R e. RR* ) |
19 |
11 8
|
sselid |
|- ( ph -> S e. A ) |
20 |
3 19
|
ffvelrnd |
|- ( ph -> ( F ` S ) e. RR* ) |
21 |
20
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` S ) e. RR* ) |
22 |
3
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> F : A --> RR* ) |
23 |
22 17
|
ffvelrnd |
|- ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) e. RR* ) |
24 |
8 6
|
eleqtrdi |
|- ( ph -> S e. { x e. A | R < ( F ` x ) } ) |
25 |
|
nfrab1 |
|- F/_ x { x e. A | R < ( F ` x ) } |
26 |
6 25
|
nfcxfr |
|- F/_ x Y |
27 |
|
nfcv |
|- F/_ x RR* |
28 |
|
nfcv |
|- F/_ x < |
29 |
26 27 28
|
nfsup |
|- F/_ x sup ( Y , RR* , < ) |
30 |
7 29
|
nfcxfr |
|- F/_ x S |
31 |
|
nfcv |
|- F/_ x A |
32 |
|
nfcv |
|- F/_ x R |
33 |
|
nfcv |
|- F/_ x F |
34 |
33 30
|
nffv |
|- F/_ x ( F ` S ) |
35 |
32 28 34
|
nfbr |
|- F/ x R < ( F ` S ) |
36 |
|
fveq2 |
|- ( x = S -> ( F ` x ) = ( F ` S ) ) |
37 |
36
|
breq2d |
|- ( x = S -> ( R < ( F ` x ) <-> R < ( F ` S ) ) ) |
38 |
30 31 35 37
|
elrabf |
|- ( S e. { x e. A | R < ( F ` x ) } <-> ( S e. A /\ R < ( F ` S ) ) ) |
39 |
24 38
|
sylib |
|- ( ph -> ( S e. A /\ R < ( F ` S ) ) ) |
40 |
39
|
simprd |
|- ( ph -> R < ( F ` S ) ) |
41 |
40
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> R < ( F ` S ) ) |
42 |
19
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> S e. A ) |
43 |
4
|
r19.21bi |
|- ( ( ph /\ x e. A ) -> A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) |
44 |
17 43
|
syldan |
|- ( ( ph /\ x e. ( I i^i A ) ) -> A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) |
45 |
42 44
|
jca |
|- ( ( ph /\ x e. ( I i^i A ) ) -> ( S e. A /\ A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) ) |
46 |
|
mnfxr |
|- -oo e. RR* |
47 |
46
|
a1i |
|- ( ( ph /\ x e. ( I i^i A ) ) -> -oo e. RR* ) |
48 |
|
ressxr |
|- RR C_ RR* |
49 |
13 8
|
sseldd |
|- ( ph -> S e. RR ) |
50 |
48 49
|
sselid |
|- ( ph -> S e. RR* ) |
51 |
50
|
adantr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> S e. RR* ) |
52 |
|
elinel1 |
|- ( x e. ( I i^i A ) -> x e. I ) |
53 |
52 9
|
eleqtrdi |
|- ( x e. ( I i^i A ) -> x e. ( -oo (,] S ) ) |
54 |
53
|
adantl |
|- ( ( ph /\ x e. ( I i^i A ) ) -> x e. ( -oo (,] S ) ) |
55 |
|
iocleub |
|- ( ( -oo e. RR* /\ S e. RR* /\ x e. ( -oo (,] S ) ) -> x <_ S ) |
56 |
47 51 54 55
|
syl3anc |
|- ( ( ph /\ x e. ( I i^i A ) ) -> x <_ S ) |
57 |
|
breq2 |
|- ( y = S -> ( x <_ y <-> x <_ S ) ) |
58 |
|
fveq2 |
|- ( y = S -> ( F ` y ) = ( F ` S ) ) |
59 |
58
|
breq1d |
|- ( y = S -> ( ( F ` y ) <_ ( F ` x ) <-> ( F ` S ) <_ ( F ` x ) ) ) |
60 |
57 59
|
imbi12d |
|- ( y = S -> ( ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) <-> ( x <_ S -> ( F ` S ) <_ ( F ` x ) ) ) ) |
61 |
60
|
rspcva |
|- ( ( S e. A /\ A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) -> ( x <_ S -> ( F ` S ) <_ ( F ` x ) ) ) |
62 |
45 56 61
|
sylc |
|- ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` S ) <_ ( F ` x ) ) |
63 |
18 21 23 41 62
|
xrltletrd |
|- ( ( ph /\ x e. ( I i^i A ) ) -> R < ( F ` x ) ) |
64 |
17 63
|
jca |
|- ( ( ph /\ x e. ( I i^i A ) ) -> ( x e. A /\ R < ( F ` x ) ) ) |
65 |
6
|
rabeq2i |
|- ( x e. Y <-> ( x e. A /\ R < ( F ` x ) ) ) |
66 |
64 65
|
sylibr |
|- ( ( ph /\ x e. ( I i^i A ) ) -> x e. Y ) |
67 |
66
|
ex |
|- ( ph -> ( x e. ( I i^i A ) -> x e. Y ) ) |
68 |
1 67
|
ralrimi |
|- ( ph -> A. x e. ( I i^i A ) x e. Y ) |
69 |
|
nfv |
|- F/ x z e. ( I i^i A ) |
70 |
69
|
nfci |
|- F/_ x ( I i^i A ) |
71 |
70 26
|
dfss3f |
|- ( ( I i^i A ) C_ Y <-> A. x e. ( I i^i A ) x e. Y ) |
72 |
68 71
|
sylibr |
|- ( ph -> ( I i^i A ) C_ Y ) |
73 |
15 72
|
eqssd |
|- ( ph -> Y = ( I i^i A ) ) |