Step |
Hyp |
Ref |
Expression |
1 |
|
o1lo1.1 |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
2 |
|
o1dm |
|- ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR ) |
3 |
2
|
a1i |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR ) ) |
4 |
|
lo1dm |
|- ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR ) |
5 |
4
|
adantr |
|- ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) -> dom ( x e. A |-> B ) C_ RR ) |
6 |
5
|
a1i |
|- ( ph -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) -> dom ( x e. A |-> B ) C_ RR ) ) |
7 |
1
|
ralrimiva |
|- ( ph -> A. x e. A B e. RR ) |
8 |
|
dmmptg |
|- ( A. x e. A B e. RR -> dom ( x e. A |-> B ) = A ) |
9 |
7 8
|
syl |
|- ( ph -> dom ( x e. A |-> B ) = A ) |
10 |
9
|
sseq1d |
|- ( ph -> ( dom ( x e. A |-> B ) C_ RR <-> A C_ RR ) ) |
11 |
|
simpr |
|- ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> m e. RR ) |
12 |
1
|
adantlr |
|- ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> B e. RR ) |
13 |
12
|
adantlr |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> B e. RR ) |
14 |
|
simplr |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> m e. RR ) |
15 |
13 14
|
absled |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( abs ` B ) <_ m <-> ( -u m <_ B /\ B <_ m ) ) ) |
16 |
|
ancom |
|- ( ( -u m <_ B /\ B <_ m ) <-> ( B <_ m /\ -u m <_ B ) ) |
17 |
|
lenegcon1 |
|- ( ( m e. RR /\ B e. RR ) -> ( -u m <_ B <-> -u B <_ m ) ) |
18 |
14 13 17
|
syl2anc |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( -u m <_ B <-> -u B <_ m ) ) |
19 |
18
|
anbi2d |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( B <_ m /\ -u m <_ B ) <-> ( B <_ m /\ -u B <_ m ) ) ) |
20 |
16 19
|
syl5bb |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( -u m <_ B /\ B <_ m ) <-> ( B <_ m /\ -u B <_ m ) ) ) |
21 |
15 20
|
bitrd |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( abs ` B ) <_ m <-> ( B <_ m /\ -u B <_ m ) ) ) |
22 |
21
|
imbi2d |
|- ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( c <_ x -> ( abs ` B ) <_ m ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
23 |
22
|
ralbidva |
|- ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
24 |
23
|
rexbidv |
|- ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
25 |
24
|
biimpd |
|- ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
26 |
|
breq2 |
|- ( n = m -> ( B <_ n <-> B <_ m ) ) |
27 |
26
|
anbi1d |
|- ( n = m -> ( ( B <_ n /\ -u B <_ p ) <-> ( B <_ m /\ -u B <_ p ) ) ) |
28 |
27
|
imbi2d |
|- ( n = m -> ( ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) ) ) |
29 |
28
|
rexralbidv |
|- ( n = m -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) ) ) |
30 |
|
breq2 |
|- ( p = m -> ( -u B <_ p <-> -u B <_ m ) ) |
31 |
30
|
anbi2d |
|- ( p = m -> ( ( B <_ m /\ -u B <_ p ) <-> ( B <_ m /\ -u B <_ m ) ) ) |
32 |
31
|
imbi2d |
|- ( p = m -> ( ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
33 |
32
|
rexralbidv |
|- ( p = m -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) ) |
34 |
29 33
|
rspc2ev |
|- ( ( m e. RR /\ m e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) |
35 |
34
|
3anidm12 |
|- ( ( m e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) |
36 |
11 25 35
|
syl6an |
|- ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) ) |
37 |
36
|
rexlimdva |
|- ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) ) |
38 |
|
simplrr |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ n <_ p ) -> p e. RR ) |
39 |
|
simplrl |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ -. n <_ p ) -> n e. RR ) |
40 |
38 39
|
ifclda |
|- ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> if ( n <_ p , p , n ) e. RR ) |
41 |
|
max2 |
|- ( ( n e. RR /\ p e. RR ) -> p <_ if ( n <_ p , p , n ) ) |
42 |
41
|
ad2antlr |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> p <_ if ( n <_ p , p , n ) ) |
43 |
12
|
adantlr |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> B e. RR ) |
44 |
43
|
renegcld |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> -u B e. RR ) |
45 |
|
simplrr |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> p e. RR ) |
46 |
|
simplrl |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> n e. RR ) |
47 |
45 46
|
ifcld |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> if ( n <_ p , p , n ) e. RR ) |
48 |
|
letr |
|- ( ( -u B e. RR /\ p e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( ( -u B <_ p /\ p <_ if ( n <_ p , p , n ) ) -> -u B <_ if ( n <_ p , p , n ) ) ) |
49 |
44 45 47 48
|
syl3anc |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( -u B <_ p /\ p <_ if ( n <_ p , p , n ) ) -> -u B <_ if ( n <_ p , p , n ) ) ) |
50 |
42 49
|
mpan2d |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ p -> -u B <_ if ( n <_ p , p , n ) ) ) |
51 |
|
lenegcon1 |
|- ( ( B e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( -u B <_ if ( n <_ p , p , n ) <-> -u if ( n <_ p , p , n ) <_ B ) ) |
52 |
43 47 51
|
syl2anc |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ if ( n <_ p , p , n ) <-> -u if ( n <_ p , p , n ) <_ B ) ) |
53 |
50 52
|
sylibd |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ p -> -u if ( n <_ p , p , n ) <_ B ) ) |
54 |
|
max1 |
|- ( ( n e. RR /\ p e. RR ) -> n <_ if ( n <_ p , p , n ) ) |
55 |
54
|
ad2antlr |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> n <_ if ( n <_ p , p , n ) ) |
56 |
|
letr |
|- ( ( B e. RR /\ n e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( ( B <_ n /\ n <_ if ( n <_ p , p , n ) ) -> B <_ if ( n <_ p , p , n ) ) ) |
57 |
43 46 47 56
|
syl3anc |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ n <_ if ( n <_ p , p , n ) ) -> B <_ if ( n <_ p , p , n ) ) ) |
58 |
55 57
|
mpan2d |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( B <_ n -> B <_ if ( n <_ p , p , n ) ) ) |
59 |
53 58
|
anim12d |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( -u B <_ p /\ B <_ n ) -> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) ) |
60 |
59
|
ancomsd |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ -u B <_ p ) -> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) ) |
61 |
43 47
|
absled |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( abs ` B ) <_ if ( n <_ p , p , n ) <-> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) ) |
62 |
60 61
|
sylibrd |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ -u B <_ p ) -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) |
63 |
62
|
imim2d |
|- ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) ) |
64 |
63
|
ralimdva |
|- ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) ) |
65 |
64
|
reximdv |
|- ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) ) |
66 |
|
breq2 |
|- ( m = if ( n <_ p , p , n ) -> ( ( abs ` B ) <_ m <-> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) |
67 |
66
|
imbi2d |
|- ( m = if ( n <_ p , p , n ) -> ( ( c <_ x -> ( abs ` B ) <_ m ) <-> ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) ) |
68 |
67
|
rexralbidv |
|- ( m = if ( n <_ p , p , n ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) ) |
69 |
68
|
rspcev |
|- ( ( if ( n <_ p , p , n ) e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) |
70 |
40 65 69
|
syl6an |
|- ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) ) |
71 |
70
|
rexlimdvva |
|- ( ( ph /\ A C_ RR ) -> ( E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) ) |
72 |
37 71
|
impbid |
|- ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) ) |
73 |
|
rexanre |
|- ( A C_ RR -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
74 |
73
|
adantl |
|- ( ( ph /\ A C_ RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
75 |
74
|
2rexbidv |
|- ( ( ph /\ A C_ RR ) -> ( E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
76 |
72 75
|
bitrd |
|- ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
77 |
|
reeanv |
|- ( E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) |
78 |
76 77
|
bitrdi |
|- ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
79 |
|
rexcom |
|- ( E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) |
80 |
|
rexcom |
|- ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) <-> E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) ) |
81 |
|
rexcom |
|- ( E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) <-> E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) |
82 |
80 81
|
anbi12i |
|- ( ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) |
83 |
78 79 82
|
3bitr4g |
|- ( ( ph /\ A C_ RR ) -> ( E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
84 |
|
simpr |
|- ( ( ph /\ A C_ RR ) -> A C_ RR ) |
85 |
12
|
recnd |
|- ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> B e. CC ) |
86 |
84 85
|
elo1mpt |
|- ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. O(1) <-> E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) ) |
87 |
84 12
|
ello1mpt |
|- ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. <_O(1) <-> E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) ) ) |
88 |
12
|
renegcld |
|- ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> -u B e. RR ) |
89 |
84 88
|
ello1mpt |
|- ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> -u B ) e. <_O(1) <-> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) |
90 |
87 89
|
anbi12d |
|- ( ( ph /\ A C_ RR ) -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) <-> ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) ) |
91 |
83 86 90
|
3bitr4d |
|- ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) |
92 |
91
|
ex |
|- ( ph -> ( A C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) ) |
93 |
10 92
|
sylbid |
|- ( ph -> ( dom ( x e. A |-> B ) C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) ) |
94 |
3 6 93
|
pm5.21ndd |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) |